@[inline, reducible]
A general abstraction for the idea of a scope in the compiler.
Instances For
Instances For
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.
Instances For
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.
Instances For
Check whether fvarId
is in the current scope, that is, was declared within
the current fun
declaration that is being processed.
Instances For
Add a new FVarId
to the current scope.