Documentation

Lean.Elab.Level

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