# Documentation

Lean.Compiler.LCNF.InferType

# Type inference for LCNF #

@[inline]

We use a regular local context to store temporary local declarations created during type inference.

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.InferType.withLocalDecl {α : Type} (binderName : Lean.Name) (type : Lean.Expr) (binderInfo : Lean.BinderInfo) :
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.
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.
def Lean.Compiler.LCNF.inferAppType (fnType : Lean.Expr) (args : ) :
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.
Equations
• One or more equations did not get rendered due to their size.
• = pure c.resultType
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.
def Lean.Compiler.LCNF.mkAuxFunDecl (params : ) (code : Lean.Compiler.LCNF.Code) (prefixName : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.mkAuxJpDecl (params : ) (code : Lean.Compiler.LCNF.Code) (prefixName : ) :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.isErasedCompatible (type : Lean.Expr) (predVars : optParam () #[]) :

Return true if type should be erased. See item 1 in the note above where x ◾ ◾ is a proposition and should be erased when the universe level parameter is set to 0.

Remark: predVars is a bitmask that indicates whether de-bruijn variables are predicates or not. That is, #i is a predicate if predVars[predVars.size - i - 1] = true

Equations
partial def Lean.Compiler.LCNF.isErasedCompatible.go (type : Lean.Expr) (predVars : ) :

Return true if the given LCNF are equivalent. List Nat and (fun x => List x) Nat are both equivalent.