@[inline, reducible]

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 α

@[inline, reducible]

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.instMonadScope m n = { getScope := liftM Lean.Compiler.LCNF.getScope, withScope := fun {α} f => monadMap fun {β} => Lean.Compiler.LCNF.withScope f }

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

• Lean.Compiler.LCNF.withParams ps x = Lean.Compiler.LCNF.withScope (fun s => Array.foldl (fun s p => Lean.FVarIdSet.insert s p.fvarId) s ps 0 (Array.size ps)) x

@[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.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 => ∅) x