Documentation

Lean.Elab.Level

source
structure Lean.Elab.Level.Context :
Type
Instances For
    source
    structure Lean.Elab.Level.State :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Lean.Elab.Level.LevelElabM (α : Type) :
      Type
      Instances For
        source
        instance Lean.Elab.Level.instMonadOptionsLevelElabM :
        Lean.MonadOptions Lean.Elab.Level.LevelElabM
        source
        @[always_inline]
        instance Lean.Elab.Level.instMonadRefLevelElabM :
        Lean.MonadRef Lean.Elab.Level.LevelElabM
        source
        instance Lean.Elab.Level.instAddMessageContextLevelElabM :
        Lean.AddMessageContext Lean.Elab.Level.LevelElabM
        source
        @[always_inline]
        instance Lean.Elab.Level.instMonadNameGeneratorLevelElabM :
        Lean.MonadNameGenerator Lean.Elab.Level.LevelElabM
        source
        def Lean.Elab.Level.mkFreshLevelMVar :
        Lean.Elab.Level.LevelElabM Lean.Level
        Instances For
          source
          opaque Lean.Elab.Level.maxUniverseOffset :
          Lean.Option Nat
          source
          partial def Lean.Elab.Level.elabLevel (stx : Lean.Syntax) :
          Lean.Elab.Level.LevelElabM Lean.Level