There are many resources (1, 2, 3, 4) to learn about various techniques for manipulating syntax with variable binding, however, I haven't seen many descriptions of which specific techniques are actually used in existing proof assistants. Is there some existing chart for this kind of information, or is it "folklore"?

  • 1
    $\begingroup$ @GuyCoder The linked answer has an accepted answer now. $\endgroup$
    – march
    Feb 23, 2022 at 7:00


Browse other questions tagged or ask your own question.