Documentation
Lean
.
Compiler
.
LCNF
.
ToImpure
Search
return to top
source
Imports
Init.Data.Format.Macro
Lean.Compiler.LCNF.PassManager
Lean.Compiler.LCNF.PhaseExt
Lean.Compiler.LCNF.ToImpureType
Imported by
Lean
.
Compiler
.
LCNF
.
lowerResultType
Lean
.
Compiler
.
LCNF
.
toImpure
source
def
Lean
.
Compiler
.
LCNF
.
lowerResultType
(
type
:
Expr
)
(
arity
:
Nat
)
:
CoreM
Expr
Equations
Lean.Compiler.LCNF.lowerResultType
type
arity
=
Lean.Compiler.LCNF.toImpureType
(
Lean.Compiler.LCNF.lowerResultType.resultTypeForArity✝
type
arity
)
Instances For
source
def
Lean
.
Compiler
.
LCNF
.
toImpure
:
Pass
Equations
One or more equations did not get rendered due to their size.
Instances For