@[reducible, inline]

abbrev Lean.Compiler.LCNF.Scope : Type

Equations

• Lean.Compiler.LCNF.Scope = Lean.FVarIdSet

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

• getScope : m Lean.Compiler.LCNF.Scope
• withScope : {α : Type} → (Lean.Compiler.LCNF.Scope → Lean.Compiler.LCNF.Scope) → m α → m α

Instances

• Lean.Compiler.LCNF.Specialize.instMonadScopeSpecializeM
• Lean.Compiler.LCNF.instMonadScopeOfMonadLiftOfMonadFunctor
• Lean.Compiler.LCNF.instMonadScopeScopeTOfMonad

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.ScopeT m = ReaderT Lean.Compiler.LCNF.Scope m

Instances For

• Lean.Compiler.LCNF.instMonadScopeScopeTOfMonad

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

Equations

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

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

Equations

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

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

Equations

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

@[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 α

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Compiler.LCNF.withNewScope x = Lean.Compiler.LCNF.withScope (fun (x : Lean.Compiler.LCNF.Scope) => ∅) x