Documentation

Lean.Compiler.LCNF.Internalize

@[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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Refresh free variables ids in code, and store their declarations in the local context.

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