Lean.Compiler.LCNF.Internalize

source

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Internalize.InternalizeM (α : Type) :

Type

Equations

Instances For

source

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue :

MonadFVarSubst InternalizeM true

The InternalizeM monad is a translator. It "translates" the free variables in the input expressions and Code, into new fresh free variables in the local context.

Equations

source

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM :

MonadFVarSubstState InternalizeM

Equations

source

def Lean.Compiler.LCNF.Internalize.internalizeParam (p : Param) :

InternalizeM Param

Equations

Instances For

source

def Lean.Compiler.LCNF.Internalize.internalizeLetDecl (decl : LetDecl) :

InternalizeM LetDecl

Equations

Instances For

source

partial def Lean.Compiler.LCNF.Internalize.internalizeFunDecl (decl : FunDecl) :

InternalizeM FunDecl

source

partial def Lean.Compiler.LCNF.Internalize.internalizeCode (code : Code) :

InternalizeM Code

source

def Lean.Compiler.LCNF.Internalize.internalizeCodeDecl (decl : CodeDecl) :

InternalizeM CodeDecl

Equations

Instances For

source

def Lean.Compiler.LCNF.Code.internalize (code : Code) (s : FVarSubst := ∅) :

CompilerM Code

Refresh free variables ids in code, and store their declarations in the local context.

Equations

Instances For

source

def Lean.Compiler.LCNF.Decl.internalize (decl : Decl) (s : FVarSubst := ∅) :

CompilerM Decl

Equations

Instances For

source

def Lean.Compiler.LCNF.Decl.internalize.go (decl : Decl) :

Internalize.InternalizeM Decl

Equations

Instances For

source

def Lean.Compiler.LCNF.cleanup (decl : Array Decl) :

CompilerM (Array Decl)

Create a fresh local context and internalize the given decls.

Equations

Instances For

source

def Lean.Compiler.LCNF.normalizeFVarIds (decl : Decl) :

CoreM Decl

Equations

Instances For