Changes between Version 32 and Version 33 of WikiStart
 Timestamp:
 Jun 9, 2014, 10:40:53 PM (6 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 reused. For more details see the blog post [http://discipledevel.blogspot.com.au/2011/08/howilearnedtostopworryingandlove.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 lemmaspecific 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 lemmaspecific LTac code to make it smaller. 6 6 7 7 Style guidelines: