Changes between Version 22 and Version 23 of WikiStart
 Timestamp:
 Jan 1, 2013, 4:18:01 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

WikiStart
v22 v23 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/ 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 trickyLTac code to make it smaller.5 The proofs 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 lemmaspecific LTac code to make it smaller. 6 6 7 7 Style guidelines: