Documentation

Lean.Elab.Level

structure Lean.Elab.Level.Context:

Type

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

structure Lean.Elab.Level.State:

Type

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

Equations

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

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 => pure msg }

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