- getScope : m Lean.Compiler.LCNF.Scope
- withScope : {α : Type} → (Lean.Compiler.LCNF.Scope → Lean.Compiler.LCNF.Scope) → m α → m α
Instances
instance
Lean.Compiler.LCNF.instMonadScope
(m : Type → Type)
(n : Type → Type)
[MonadLift m n]
[MonadFunctor m n]
[Lean.Compiler.LCNF.MonadScope m]
:
def
Lean.Compiler.LCNF.inScope
{m : Type → Type}
[Lean.Compiler.LCNF.MonadScope m]
[Monad m]
(fvarId : Lean.FVarId)
:
m Bool
Instances For
@[inline]
def
Lean.Compiler.LCNF.withParams
{m : Type → Type}
{α : Type}
[Lean.Compiler.LCNF.MonadScope m]
[Monad m]
(ps : Array Lean.Compiler.LCNF.Param)
(x : m α)
:
m α
Instances For
@[inline]
def
Lean.Compiler.LCNF.withFVar
{m : Type → Type}
{α : Type}
[Lean.Compiler.LCNF.MonadScope m]
[Monad m]
(fvarId : Lean.FVarId)
(x : m α)
:
m α
Instances For
@[inline]
def
Lean.Compiler.LCNF.withNewScope
{m : Type → Type}
{α : Type}
[Lean.Compiler.LCNF.MonadScope m]
[Monad m]
(x : m α)
:
m α