# Documentation

Lean.Compiler.LCNF.Bind

• codeBind :

Helper class for lifting CompilerM.codeBind

Instances
@[inline]
abbrev Lean.Compiler.LCNF.Code.bind {m : } [inst : ] (f : ) :

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.

Equations
instance Lean.Compiler.LCNF.instMonadCodeBindReaderT {m : } {ρ : Type} [inst : ] :
Equations
instance Lean.Compiler.LCNF.instMonadCodeBindStateRefT' {ω : Type} {m : } {σ : Type} [inst : STWorld ω m] [inst : ] :
Equations

Create new parameters for the given arrow type. Example: if type is Nat → Bool → Int, the result is an array containing two new parameters with types Nat and Bool.

Equations
partial def Lean.Compiler.LCNF.mkNewParams.go (type : Lean.Expr) (xs : ) :
Equations
• = let typeArity := ; let valueArity := Array.size params; decide (typeArity > valueArity)
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.