source
structure Lean.Elab.Level.Context :
Type

- options : Options
- ref : Syntax
- autoBoundImplicit : Bool

Instances For

source
structure Lean.Elab.Level.State :
Type

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

Instances For

source
@[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)

Instances For

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

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

source
@[always_inline]
instance Lean.Elab.Level.instMonadRefLevelElabM :
MonadRef LevelElabM
Equations

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

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

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

source
@[always_inline]
instance Lean.Elab.Level.instMonadNameGeneratorLevelElabM :
MonadNameGenerator LevelElabM
Equations

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

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

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

Instances For

source
opaque Lean.Elab.Level.maxUniverseOffset :
Lean.Option Nat
source
partial def Lean.Elab.Level.elabLevel (stx : Syntax) :
LevelElabM Level