Documentation

Lean.Util.CollectLevelParams

source
structure Lean.CollectLevelParams.State :
Type
Instances For
    source
    @[implicit_reducible]
    instance Lean.CollectLevelParams.instInhabitedState :
    Inhabited State
    source
    @[reducible, inline]
    abbrev Lean.CollectLevelParams.Visitor :
    Type
    Instances For
      source
      partial def Lean.CollectLevelParams.visitLevel (u : Level) :
      Visitor
      source
      partial def Lean.CollectLevelParams.collect :
      Level → Visitor
      source
      def Lean.CollectLevelParams.visitLevels (us : List Level) :
      Visitor
      Instances For
        source
        partial def Lean.CollectLevelParams.visitExpr (e : Expr) :
        Visitor
        source
        partial def Lean.CollectLevelParams.main :
        Expr → Visitor
        source
        def Lean.CollectLevelParams.State.getUnusedLevelParam (s : State) (pre : Name := `v) :
        Level
        Instances For
          source
          def Lean.collectLevelParams (s : CollectLevelParams.State) (e : Expr) :
          CollectLevelParams.State
          Instances For
            source
            def Lean.CollectLevelParams.State.collect (s : State) (e : Expr) :
            State
            Instances For