Documentation

Lean.Util.CollectLevelParams

structure Lean.CollectLevelParams.State :

Type

visitedLevel : Lean.LevelSet
visitedExpr : Lean.ExprSet
params : Array Lean.Name

instance Lean.CollectLevelParams.instInhabitedState :

Inhabited Lean.CollectLevelParams.State

Equations

Lean.CollectLevelParams.instInhabitedState = { default := { visitedLevel := ∅, visitedExpr := ∅, params := #[] } }

@[inline]

abbrev Lean.CollectLevelParams.Visitor :

Type

Equations

Lean.CollectLevelParams.Visitor = (Lean.CollectLevelParams.State → Lean.CollectLevelParams.State)

partial def Lean.CollectLevelParams.visitLevel (u : Lean.Level) :

Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.collect :

Lean.Level → Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.visitExpr (e : Lean.Expr) :

Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.main :

Lean.Expr → Lean.CollectLevelParams.Visitor

def Lean.CollectLevelParams.State.getUnusedLevelParam (s : Lean.CollectLevelParams.State) (pre : optParam Lean.Name `v) :

Equations

Lean.CollectLevelParams.State.getUnusedLevelParam s pre = let v := Lean.mkLevelParam pre; if Std.HashSet.contains s.visitedLevel v = true then (fun loop => loop 1) (Lean.CollectLevelParams.State.getUnusedLevelParam.loop s pre) else v

partial def Lean.CollectLevelParams.State.getUnusedLevelParam.loop (s : Lean.CollectLevelParams.State) (pre : optParam Lean.Name `v) (i : Nat) :

def Lean.collectLevelParams (s : Lean.CollectLevelParams.State) (e : Lean.Expr) :

Lean.CollectLevelParams.State

Equations

Lean.collectLevelParams s e = Lean.CollectLevelParams.main e s

def Lean.CollectLevelParams.State.collect (s : Lean.CollectLevelParams.State) (e : Lean.Expr) :

Lean.CollectLevelParams.State

Equations

Lean.CollectLevelParams.State.collect s e = Lean.collectLevelParams s e