Documentation

Lean.Compiler.LCNF.InferType

Type inference for LCNF #

@[inline, reducible]

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

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

Equations

Lean.Compiler.LCNF.InferType.InferTypeM = ReaderT Lean.LocalContext Lean.Compiler.LCNF.CompilerM

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lake.Name

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

@[inline]

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

Lean.Compiler.LCNF.InferType.InferTypeM α

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.InferType.InferTypeM (Option Lean.Level)

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Level

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.let decl k) = Lean.Compiler.LCNF.Code.inferType k
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.fun decl k) = Lean.Compiler.LCNF.Code.inferType k
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.jp decl k) = Lean.Compiler.LCNF.Code.inferType k
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.return fvarId) = Lean.Compiler.LCNF.getType fvarId
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.unreach type) = pure type
Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.Code.cases c) = pure c.resultType

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

def Lean.Compiler.LCNF.AltCore.inferType (alt : Lean.Compiler.LCNF.Alt) :

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

Lean.Compiler.LCNF.AltCore.inferType alt = Lean.Compiler.LCNF.Code.inferType (Lean.Compiler.LCNF.AltCore.getCode alt)

Instances For

def Lean.Compiler.LCNF.mkAuxLetDecl (e : Lean.Compiler.LCNF.LetValue) (prefixName : optParam Lake.Name `_x) :

Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

def Lean.Compiler.LCNF.mkAuxFunDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lake.Name `_f) :

Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

Equations

One or more equations did not get rendered due to their size.

Instances For

def Lean.Compiler.LCNF.mkAuxJpDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lake.Name `_jp) :

Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

Equations

Lean.Compiler.LCNF.mkAuxJpDecl params code prefixName = Lean.Compiler.LCNF.mkAuxFunDecl params code prefixName

Instances For

def Lean.Compiler.LCNF.mkAuxJpDecl' (param : Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lake.Name `_jp) :

Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

Equations

Lean.Compiler.LCNF.mkAuxJpDecl' param code prefixName = let params := #[param]; Lean.Compiler.LCNF.mkAuxFunDecl params code prefixName

Instances For

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

Lean.Compiler.LCNF.CompilerM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Lean.Compiler.LCNF.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

Equations

Lean.Compiler.LCNF.isErasedCompatible type predVars = Lean.Compiler.LCNF.isErasedCompatible.go type predVars

Instances For

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

Lean.Compiler.LCNF.CompilerM Bool

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

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