Changes between Version 3 and Version 4 of WikiStart

Timestamp:

Dec 27, 2012, 2:20:39 PM (12 years ago)

Author:

benl

Comment:

--

WikiStart

@@ -2 +2 @@
 
 Iron Lambda is a collection of Coq formalisations for functional languages
-of various complexities. The aim of the project was to get the proofs done
-and not worry much about using the coolest new approaches.
+of various complexities. The aim of the project is to get the proofs done
+and not worry too much about using the coolest new approaches. 
 
-All proofs use straight deBruijn indices for binders, which aren't too bad
-once you understand what lifting lemmas are required. They use a 
-"semi-Chilpala" 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.
+All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They use a "semi-Chilpala" 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.
 
 Style guidelines:
@@ -18 +13 @@
  
 * No unicode or infix operators for judgement forms.
-  When *I* use them in *my* proofs they make perfect sense, but when you
+  When ''I'' use them in ''my'' proofs they make perfect sense, but when you
   use them in yours they're completely unreadable.
 
 * Heavy use of the 'burn' megatactic. This is in the same vein as Chilpala's
- 'crush' tactic, but I couldn't work out what 'crush' was doing...
+ 'crush' tactic, but at the time I couldn't work out what 'crush' was doing...
 
 * Uses the 'Case' meta-tactic to add structure.