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
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Elab.Level.instMonadOptionsLevelElabM :
        MonadOptions LevelElabM
        source
        @[implicit_reducible, always_inline]
        instance Lean.Elab.Level.instMonadRefLevelElabM :
        MonadRef LevelElabM
        source
        @[implicit_reducible]
        instance Lean.Elab.Level.instAddMessageContextLevelElabM :
        AddMessageContext LevelElabM
        source
        @[implicit_reducible, always_inline]
        instance Lean.Elab.Level.instMonadNameGeneratorLevelElabM :
        MonadNameGenerator LevelElabM
        source
        def Lean.Elab.Level.mkFreshLevelMVar :
        LevelElabM Level
        Instances For
          source
          opaque Lean.Elab.Level.maxUniverseOffset :
          Lean.Option Nat
          source
          partial def Lean.Elab.Level.elabLevel (stx : Syntax) :
          LevelElabM Level