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