# Documentation

Lean.Compiler.LCNF.AlphaEqv

Alpha equivalence for LCNF Code

@[inline]
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Compiler.LCNF.AlphaEqv.withFVar {α : Type} (fvarId₁ : Lean.FVarId) (fvarId₂ : Lean.FVarId) :
Equations
@[inline]
Equations
@[specialize #[]]
def Lean.Compiler.LCNF.AlphaEqv.withParams.go (params₁ : ) (params₂ : ) (h : Array.size params₂ = Array.size params₁) (i : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Compiler.LCNF.AlphaEqv.eqvAlts (alts₁ : ) (alts₂ : ) :

Return true if c₁ and c₂ are alpha equivalent.

Equations