@[reducible, inline]

abbrev Lean.Compiler.LCNF.ScopeM (α : Type) : Type

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

def Lean.Compiler.LCNF.ScopeM.getScope : Lean.Compiler.LCNF.ScopeM Lean.FVarIdSet

def Lean.Compiler.LCNF.ScopeM.setScope (newScope : Lean.FVarIdSet) : Lean.Compiler.LCNF.ScopeM Unit

Equations

• Lean.Compiler.LCNF.ScopeM.setScope newScope = set newScope

def Lean.Compiler.LCNF.ScopeM.clearScope : Lean.Compiler.LCNF.ScopeM Unit

Equations

• Lean.Compiler.LCNF.ScopeM.clearScope = Lean.Compiler.LCNF.ScopeM.setScope ∅

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

• Lean.Compiler.LCNF.ScopeM.withBackTrackingScope x = do let scope ← liftM Lean.Compiler.LCNF.ScopeM.getScope tryFinally x (liftM (Lean.Compiler.LCNF.ScopeM.setScope scope))

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.

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.

def Lean.Compiler.LCNF.ScopeM.addToScope (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.ScopeM Unit

Add a new FVarId to the current scope.

Equations

• Lean.Compiler.LCNF.ScopeM.addToScope fvarId = modify fun (scope : Lean.FVarIdSet) => scope.insert fvarId