Changes between Version 4 and Version 5 of WikiStart
- Timestamp:
- Dec 27, 2012, 2:21:45 PM (12 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
WikiStart
v4 v5 5 5 and not worry too much about using the coolest new approaches. 6 6 7 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.7 All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They use a "semi-[http://adam.chlipala.net/cpdt/ 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. 8 8 9 9 Style guidelines:
