@[reducible, inline]

abbrev Lean.Compiler.LCNF.Scope : Type

Equations

• Eq Lean.Compiler.LCNF.Scope Lean.FVarIdSet

structure 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

Equations

• Eq (Lean.Compiler.LCNF.ScopeT m) (ReaderT Lean.Compiler.LCNF.Scope m)

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

Equations

• Eq Lean.Compiler.LCNF.instMonadScopeScopeTOfMonad { getScope := MonadReader.read, withScope := fun {α : Type} => MonadWithReader.withReader }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Eq (Lean.Compiler.LCNF.inScope fvarId) do let __do_lift ← Lean.Compiler.LCNF.MonadScope.getScope Pure.pure (Lean.RBTree.contains __do_lift fvarId)

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Eq (Lean.Compiler.LCNF.withFVar fvarId x) (Lean.Compiler.LCNF.MonadScope.withScope (fun (s : Lean.Compiler.LCNF.Scope) => Lean.FVarIdSet.insert s fvarId) x)

@[inline]

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

Equations

• Eq (Lean.Compiler.LCNF.withNewScope x) (Lean.Compiler.LCNF.MonadScope.withScope (fun (x : Lean.Compiler.LCNF.Scope) => EmptyCollection.emptyCollection) x)