structure Lean.Elab.Level.Context : Type

• options : Lean.Options
• ref : Lean.Syntax
• autoBoundImplicit : Bool

structure Lean.Elab.Level.State : Type

• ngen : Lean.NameGenerator
• mctx : Lean.MetavarContext
• levelNames : List Lake.Name

@[inline, reducible]

abbrev Lean.Elab.Level.LevelElabM (α : Type) : Type

Equations

• Lean.Elab.Level.LevelElabM = ReaderT Lean.Elab.Level.Context (EStateM Lean.Exception Lean.Elab.Level.State)

instance Lean.Elab.Level.instMonadOptionsLevelElabM : Lean.MonadOptions Lean.Elab.Level.LevelElabM

Equations

• Lean.Elab.Level.instMonadOptionsLevelElabM = { getOptions := do let __do_lift ← read pure __do_lift.options }

@[always_inline]

instance Lean.Elab.Level.instMonadRefLevelElabM : Lean.MonadRef Lean.Elab.Level.LevelElabM

Equations

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

instance Lean.Elab.Level.instAddMessageContextLevelElabM : Lean.AddMessageContext Lean.Elab.Level.LevelElabM

Equations

• Lean.Elab.Level.instAddMessageContextLevelElabM = { addMessageContext := fun (msg : Lean.MessageData) => pure msg }

@[always_inline]

instance Lean.Elab.Level.instMonadNameGeneratorLevelElabM : Lean.MonadNameGenerator Lean.Elab.Level.LevelElabM

Equations

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

def Lean.Elab.Level.mkFreshLevelMVar : Lean.Elab.Level.LevelElabM Lean.Level

Equations

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

opaque Lean.Elab.Level.maxUniverseOffset : Lean.Option Nat

partial def Lean.Elab.Level.elabLevel (stx : Lean.Syntax) : Lean.Elab.Level.LevelElabM Lean.Level