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
source
def Lean.Compiler.LCNF.ScopeM.getScope :
Lean.Compiler.LCNF.ScopeM Lean.FVarIdSet
Equations
source
def Lean.Compiler.LCNF.ScopeM.setScope (newScope : Lean.FVarIdSet) :
Lean.Compiler.LCNF.ScopeM Unit
Equations
source
def Lean.Compiler.LCNF.ScopeM.clearScope :
Lean.Compiler.LCNF.ScopeM Unit
Equations
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
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
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
source
def Lean.Compiler.LCNF.ScopeM.addToScope (fvarId : Lean.FVarId) :
Lean.Compiler.LCNF.ScopeM Unit

Add a new FVarId to the current scope.

Equations