Changes between Version 3 and Version 4 of WikiStart
 Timestamp:
 Dec 27, 2012, 2:20:39 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

WikiStart
v3 v4 2 2 3 3 Iron Lambda is a collection of Coq formalisations for functional languages 4 of various complexities. The aim of the project was to get the proofs done5 and not worry much about using the coolest new approaches.4 of various complexities. The aim of the project is to get the proofs done 5 and not worry too much about using the coolest new approaches. 6 6 7 All proofs use straight deBruijn indices for binders, which aren't too bad 8 once you understand what lifting lemmas are required. They use a 9 "semiChilpala" approach to mechanisation  most lemmas are added to the 10 global hint and rewrite databases, but if the proof script of a particular 11 lemma was already of a sane length, then we haven't invested time writing 12 tricky LTac code to make it smaller. 7 All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They use a "semiChilpala" approach to mechanisation  most lemmas are added to the global hint and rewrite databases, but if the proof script of a particular lemma was already of a sane length, then we haven't invested time writing tricky LTac code to make it smaller. 13 8 14 9 Style guidelines: … … 18 13 19 14 * No unicode or infix operators for judgement forms. 20 When *I* use them in *my*proofs they make perfect sense, but when you15 When ''I'' use them in ''my'' proofs they make perfect sense, but when you 21 16 use them in yours they're completely unreadable. 22 17 23 18 * Heavy use of the 'burn' megatactic. This is in the same vein as Chilpala's 24 'crush' tactic, but I couldn't work out what 'crush' was doing...19 'crush' tactic, but at the time I couldn't work out what 'crush' was doing... 25 20 26 21 * Uses the 'Case' metatactic to add structure.