Changes between Version 32 and Version 33 of WikiStart
- Timestamp:
- Jun 9, 2014, 10:40:53 PM (11 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
WikiStart
v32 v33 3 3 We just use straight deBruijn indices for binders. Using deBruijn indices does require that we prove some lemmas about lifting and substitution, but they are very similar between languages, so the initial effort can be re-used. For more details see the blog post [http://disciple-devel.blogspot.com.au/2011/08/how-i-learned-to-stop-worrying-and-love.html How I learned to stop worrying and love deBruijn indices.] 4 4 5 The proofs use a "semi-[http://adam.chlipala.net/cpdt/ Ch ilpala]" 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 lemma-specific LTac code to make it smaller.5 The proofs use a "semi-[http://adam.chlipala.net/cpdt/ Chlipala]" 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 lemma-specific LTac code to make it smaller. 6 6 7 7 Style guidelines:
