@[reducible, inline]
Instances For
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
- Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue = { getSubst := get }
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Compiler.LCNF.Code.internalize
(code : Lean.Compiler.LCNF.Code)
(s : Lean.Compiler.LCNF.FVarSubst := ∅)
:
Refresh free variables ids in code
, and store their declarations in the local context.
Equations
- code.internalize s = StateRefT'.run' (Lean.Compiler.LCNF.Internalize.internalizeCode code) s
Instances For
def
Lean.Compiler.LCNF.Decl.internalize
(decl : Lean.Compiler.LCNF.Decl)
(s : Lean.Compiler.LCNF.FVarSubst := ∅)
:
Instances For
Create a fresh local context and internalize the given decls.
Equations
- One or more equations did not get rendered due to their size.