Documentation

Lean.Compiler.LCNF.ScopeM

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ScopeM (α : Type) :
Type

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

Equations
Instances For
    source
    def Lean.Compiler.LCNF.ScopeM.getScope :
    ScopeM FVarIdSet
    Equations
    Instances For
      source
      def Lean.Compiler.LCNF.ScopeM.setScope (newScope : FVarIdSet) :
      ScopeM Unit
      Equations
      Instances For
        source
        def Lean.Compiler.LCNF.ScopeM.clearScope :
        ScopeM Unit
        Equations
        Instances For
          source
          def Lean.Compiler.LCNF.ScopeM.withBackTrackingScope {m : Type → Type u_1} {α : Type} [MonadLiftT ScopeM m] [Monad m] [MonadFinally m] (x : m α) :
          m α

          Execute x but recover the previous scope after doing so.

          Equations
          Instances For
            source
            def Lean.Compiler.LCNF.ScopeM.withNewScope {m : Type → Type u_1} {α : Type} [MonadLiftT ScopeM m] [Monad m] [MonadFinally m] (x : m α) :
            m α

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

            Equations
            Instances For
              source
              def Lean.Compiler.LCNF.ScopeM.isInScope (fvarId : FVarId) :
              ScopeM Bool

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

              Equations
              Instances For
                source
                def Lean.Compiler.LCNF.ScopeM.addToScope (fvarId : FVarId) :
                ScopeM Unit

                Add a new FVarId to the current scope.

                Equations
                Instances For