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 Lean.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)

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

@[always_inline]

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

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

@[always_inline]

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

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

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

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