Type inference for LCNF

@[reducible, inline]

abbrev Lean.Compiler.LCNF.InferType.InferTypeM (α : Type) : Type

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

def Lean.Compiler.LCNF.InferType.getBinderName (fvarId : FVarId) : InferTypeM Name

def Lean.Compiler.LCNF.InferType.getType (fvarId : FVarId) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.mkForallFVars (xs : Array Expr) (type : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.mkForallParams (params : Array Param) (type : Expr) : InferTypeM Expr

@[inline]

def Lean.Compiler.LCNF.InferType.withLocalDecl {α : Type} (binderName : Name) (type : Expr) (binderInfo : BinderInfo) (k : Expr → InferTypeM α) : InferTypeM α

def Lean.Compiler.LCNF.InferType.inferConstType (declName : Name) (us : List Level) : CompilerM Expr

def Lean.Compiler.LCNF.InferType.inferLitValueType (value : LitValue) : Expr

def Lean.Compiler.LCNF.InferType.inferArgType (arg : Arg) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.inferType (e : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.inferLetValueType (e : LetValue) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.inferAppTypeCore (fType : Expr) (args : Array Arg) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.inferAppType (e : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.inferProjType (structName : Name) (idx : Nat) (s : FVarId) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.getLevel? (type : Expr) : InferTypeM (Option Level)

partial def Lean.Compiler.LCNF.InferType.inferForallType (e : Expr) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.inferForallType.go (e : Expr) (fvars : Array Expr) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.inferLambdaType (e : Expr) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.inferLambdaType.go (e : Expr) (fvars all : Array Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.inferType (e : Expr) : CompilerM Expr

def Lean.Compiler.LCNF.inferAppType (fnType : Expr) (args : Array Arg) : CompilerM Expr

def Lean.Compiler.LCNF.getLevel (type : Expr) : CompilerM Level

def Lean.Compiler.LCNF.Arg.inferType (arg : Arg) : CompilerM Expr

def Lean.Compiler.LCNF.LetValue.inferType (e : LetValue) : CompilerM Expr

def Lean.Compiler.LCNF.Code.inferType (code : Code) : CompilerM Expr

def Lean.Compiler.LCNF.Code.inferParamType (params : Array Param) (code : Code) : CompilerM Expr

def Lean.Compiler.LCNF.Alt.inferType (alt : Alt) : CompilerM Expr

def Lean.Compiler.LCNF.mkAuxLetDecl (e : LetValue) (prefixName : Name := `_x) : CompilerM LetDecl

def Lean.Compiler.LCNF.mkForallParams (params : Array Param) (type : Expr) : CompilerM Expr

def Lean.Compiler.LCNF.mkAuxFunDecl (params : Array Param) (code : Code) (prefixName : Name := `_f) : CompilerM FunDecl

def Lean.Compiler.LCNF.mkAuxJpDecl (params : Array Param) (code : Code) (prefixName : Name := `_jp) : CompilerM FunDecl

def Lean.Compiler.LCNF.mkAuxJpDecl' (param : Param) (code : Code) (prefixName : Name := `_jp) : CompilerM FunDecl

def Lean.Compiler.LCNF.mkCasesResultType (alts : Array Alt) : CompilerM Expr

def Lean.Compiler.LCNF.isErasedCompatible (type : Expr) (predVars : Array Bool := #[]) : CompilerM Bool

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

partial def Lean.Compiler.LCNF.isErasedCompatible.go (type : Expr) (predVars : Array Bool) : CompilerM Bool

partial def Lean.Compiler.LCNF.eqvTypes (a b : Expr) : Bool

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