1.3. Free Variables
The set given by FV contains exactly the named variables that occur free in a term.
De Bruijn variables are bound-variable references, so they contribute no free
names.
\begin{array}{rcl}
FV(n) &=& \varnothing\\
FV(x) &=& \{x\}\\
FV(\lambda.\ e) &=& FV(e)\\
FV(e_1\ e_2) &=& FV(e_1) \cup FV(e_2)
\end{array}
This definition tracks only named free variables. Bound de Bruijn indices are not names, so they cannot contribute to this set.
def FV : L0 -> Set String
| .var _ => {}
| .free x => {x}
| .lam body => (FV body)
| .app f a => (FV f) ∪ (FV a)def Closed (t : L0) : Prop :=
∀ x, x ∉ FV texample : "x" ∈ FV L0[x] := ⊢ "x" ∈ (free "x").FV All goals completed! 🐙example : Closed L0[λ 0] := ⊢ (var 0).lam.Closed intro _ x✝:Stringh:x✝ ∈ (var 0).lam.FV⊢ False; All goals completed! 🐙