Changes between Version 32 and Version 33 of WikiStart


Ignore:
Timestamp:
Jun 9, 2014, 10:40:53 PM (10 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v32 v33  
    33We 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.]
    44
    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 lemma-specific LTac code to make it smaller.
     5The 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.
    66
    77Style guidelines: