All Questions
Tagged with binders implementation
2
questions
5
votes
2
answers
233
views
Algorithm for the locally nameless representation used by Lean
I have heard that Lean uses the locally nameless representation for handling binders, yet if I input an expression that has a bound variable in it, the bound variable is not displayed using its de ...
- 429
3
votes
0
answers
69
views
Variable binding techniques used in proof assistants? [duplicate]
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 ...
