@[reducible, inline]

abbrev Lean.Compiler.LCNF.Scope : Type

class Lean.Compiler.LCNF.MonadScope (m : Type → Type) : Type 1

• getScope : m Scope
• withScope {α : Type} : (Scope → Scope) → m α → m α

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ScopeT (m : Type → Type) (α : Type) : Type

@[implicit_reducible]

instance Lean.Compiler.LCNF.instMonadScopeScopeTOfMonad {m : Type → Type} [Monad m] : MonadScope (ScopeT m)

@[implicit_reducible]

instance Lean.Compiler.LCNF.instMonadScopeOfMonadLiftOfMonadFunctor (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadScope m] : MonadScope n

def Lean.Compiler.LCNF.inScope {m : Type → Type} [MonadScope m] [Monad m] (fvarId : FVarId) : m Bool

@[inline]

def Lean.Compiler.LCNF.withParams {m : Type → Type} {pu : Purity} {α : Type} [MonadScope m] [Monad m] (ps : Array (Param pu)) (x : m α) : m α

@[inline]

def Lean.Compiler.LCNF.withFVar {m : Type → Type} {α : Type} [MonadScope m] [Monad m] (fvarId : FVarId) (x : m α) : m α

@[inline]

def Lean.Compiler.LCNF.withNewScope {m : Type → Type} {α : Type} [MonadScope m] [Monad m] (x : m α) : m α