structure Lean.Elab.Level.Context : Type

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

structure Lean.Elab.Level.State : Type

• ngen : NameGenerator
• mctx : MetavarContext
• levelNames : List Name

@[reducible, inline]

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

Equations

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

@[implicit_reducible]

instance Lean.Elab.Level.instMonadOptionsLevelElabM : MonadOptions LevelElabM

Equations

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

@[implicit_reducible, always_inline]

instance Lean.Elab.Level.instMonadRefLevelElabM : MonadRef LevelElabM

Equations

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

@[implicit_reducible]

instance Lean.Elab.Level.instAddMessageContextLevelElabM : AddMessageContext LevelElabM

Equations

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

@[implicit_reducible, always_inline]

instance Lean.Elab.Level.instMonadNameGeneratorLevelElabM : MonadNameGenerator LevelElabM

Equations

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

def Lean.Elab.Level.mkFreshLevelMVar : LevelElabM 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 : Syntax) : LevelElabM Level