Documentation

Lean.Util.CollectLevelParams

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