Skip to main content

Questions tagged [binders]

Questions regarding binders (eg. by means of De Bruijn indices, HOAS, nominal approach) should be tagged with this.

Filter by
Sorted by
Tagged with
18 votes
2 answers
396 views

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
Wno-all's user avatar
  • 1,118
5 votes
2 answers
229 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 ...
user695931's user avatar