structure Lean.CollectLevelMVars.State : Type

• visitedLevel : Lean.LevelSet
• visitedExpr : Lean.ExprSet
• result : Array Lean.LMVarId

Instances For

• Lean.CollectLevelMVars.instInhabitedState

instance Lean.CollectLevelMVars.instInhabitedState : Inhabited Lean.CollectLevelMVars.State

Equations

• Lean.CollectLevelMVars.instInhabitedState = { default := { visitedLevel := ∅, visitedExpr := ∅, result := ∅ } }

@[reducible, inline]

abbrev Lean.CollectLevelMVars.Visitor : Type

Equations

• Lean.CollectLevelMVars.Visitor = (Lean.CollectLevelMVars.State → Lean.CollectLevelMVars.State)

partial def Lean.CollectLevelMVars.visitLevel (u : Lean.Level) : Lean.CollectLevelMVars.Visitor

partial def Lean.CollectLevelMVars.collect : Lean.Level → Lean.CollectLevelMVars.Visitor

partial def Lean.CollectLevelMVars.visitExpr (e : Lean.Expr) : Lean.CollectLevelMVars.Visitor

partial def Lean.CollectLevelMVars.main : Lean.Expr → Lean.CollectLevelMVars.Visitor

def Lean.collectLevelMVars (s : Lean.CollectLevelMVars.State) (e : Lean.Expr) : Lean.CollectLevelMVars.State

Collects all universe level metavariables present in e. Result is in Lean.CollectLevelMVars.State.result.

Equations

• Lean.collectLevelMVars s e = Lean.CollectLevelMVars.main e s