• Robbert Krebbers's avatar
    Use a named representation of binding in heap_lang. · eba4ac6e
    Robbert Krebbers authored
    We can use a named representation because we only substitute closed values. This
    idea is borrowed from Pierce's Software Foundations.
    
    The named representation has the following advantages:
    * Programs are much better readable than those using De Bruijn indexes.
    * Substitutions on closed terms (where all variables are explicit strings) can
      be performed by a mere simpl instead of Autosubst's asimpl. The performance
      of simpl seems better than asimpl.
    * Syntactic sugar refolds better.
    eba4ac6e
lifting.v 5.59 KB