@[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 Scope
• withScope {α : Type} : (Scope → Scope) → m α → m α

@[reducible, inline]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance 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

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

@[inline]

def Lean.Compiler.LCNF.withParams {m : Type → Type} {pu : Purity} {α : Type} [MonadScope m] [Monad m] (ps : Array (Param pu)) (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

• 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} [MonadScope m] [Monad m] (x : m α) : m α

Equations

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