Documentation

Lean.Compiler.LCNF.ScopeM

@[inline, reducible]

A general abstraction for the idea of a scope in the compiler.

Equations
Instances For

    Execute x but recover the previous scope after doing so.

    Equations
    Instances For

      Clear the current scope for the monadic action x, afterwards continuing with the old one.

      Equations
      Instances For

        Check whether fvarId is in the current scope, that is, was declared within the current fun declaration that is being processed.

        Equations
        Instances For

          Add a new FVarId to the current scope.

          Equations
          Instances For