Documentation

Lean.Compiler.LCNF.Bind

@[reducible, inline]

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
Instances For
    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.

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

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For