Documentation

Lean.Compiler.LCNF.Internalize

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