- codeBind : Lean.Compiler.LCNF.Code → (Lean.FVarId → m Lean.Compiler.LCNF.Code) → m Lean.Compiler.LCNF.Code
Helper class for lifting CompilerM.codeBind
Instances
@[inline, reducible]
abbrev
Lean.Compiler.LCNF.Code.bind
{m : Type → Type}
[Lean.Compiler.LCNF.MonadCodeBind m]
(c : Lean.Compiler.LCNF.Code)
(f : Lean.FVarId → m Lean.Compiler.LCNF.Code)
 :
Return code that is equivalent to c >>= f. That is, executes c, and then f x, where
x is a variable that contains the result of c's computation.
If c contains a jump to a join point jp_i not declared in c, we throw an exception because
an invalid block would be generated. It would be invalid because f would not
be applied to jp_i. Note that, we could have decided to create a copy of jp_i where we apply f to it,
by we decided to not do it to avoid code duplication.
Instances For
instance
Lean.Compiler.LCNF.instMonadCodeBindReaderT
{m : Type → Type}
{ρ : Type}
[Lean.Compiler.LCNF.MonadCodeBind m]
 :
instance
Lean.Compiler.LCNF.instMonadCodeBindStateRefT'
{ω : Type}
{m : Type → Type}
{σ : Type}
[STWorld ω m]
[Lean.Compiler.LCNF.MonadCodeBind m]
 :
partial def
Lean.Compiler.LCNF.mkNewParams.go
(type : Lean.Expr)
(xs : Array Lean.Expr)
(ps : Array Lean.Compiler.LCNF.Param)
 :
def
Lean.Compiler.LCNF.isEtaExpandCandidateCore
(type : Lean.Expr)
(params : Array Lean.Compiler.LCNF.Param)
 :
Instances For
@[inline, reducible]
Instances For
def
Lean.Compiler.LCNF.etaExpandCore
(type : Lean.Expr)
(params : Array Lean.Compiler.LCNF.Param)
(value : Lean.Compiler.LCNF.Code)
 :
Instances For
def
Lean.Compiler.LCNF.etaExpandCore?
(type : Lean.Expr)
(params : Array Lean.Compiler.LCNF.Param)
(value : Lean.Compiler.LCNF.Code)
 :