HepLean 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 :
    Lean.Compiler.LCNF.ScopeM Lean.FVarIdSet
    Equations
    Instances For
      source
      def Lean.Compiler.LCNF.ScopeM.setScope (newScope : Lean.FVarIdSet) :
      Lean.Compiler.LCNF.ScopeM Unit
      Equations
      Instances For
        source
        def Lean.Compiler.LCNF.ScopeM.clearScope :
        Lean.Compiler.LCNF.ScopeM Unit
        Equations
        Instances For
          source
          def Lean.Compiler.LCNF.ScopeM.withBackTrackingScope {m : Type → Type u_1} {α : Type} [MonadLiftT Lean.Compiler.LCNF.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 Lean.Compiler.LCNF.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 : Lean.FVarId) :
              Lean.Compiler.LCNF.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 : Lean.FVarId) :
                Lean.Compiler.LCNF.ScopeM Unit

                Add a new FVarId to the current scope.

                Equations
                Instances For