Bvars

Stream: lean4

[Marcus Rossel]

The Lean 4 Metaprogramming Book says:

If in our Expr, all bvars are bound, we say that the Expr is closed. The process of replacing all instances of an unbound bvar with an Expr is called instantiation.

Seeing as "bvar" is shorthand for "bound variable", what is an "unbound bvar"?

---

Would an example of an unbound bvar be bvar 3 in?:

lam `x (const `Nat) (bvar 3)

[Sebastian Ullrich]

Yes, if you have a bvar n nested under less than n binders, that's what the Lean code calls a loose bound variable. "Unbound" is not a great term as you implied, yeah.

[Marcus Rossel]

(deleted)

[Arthur Paulino]

"free" variables is also used a lot

[Sebastian Ullrich]

fvars that reference the local context by name are something entirely different from loose bound variables that do not properly reference anything, we need to strictly delineate between the two

[Trebor Huang]

I'm not a number, I'm a free variable!

[Jannis Limperg]

I've changed this section of the meta book to hopefully avoid the terminological confusion.