← Copula mathematical handbook

structure Lean.CollectLevelMVars.State : Type

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

@[instance_reducible]

instance Lean.CollectLevelMVars.instInhabitedState : Inhabited State

Equations

• Lean.CollectLevelMVars.instInhabitedState = { default := { } }

@[reducible, inline]

abbrev Lean.CollectLevelMVars.Visitor : Type

Equations

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

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

partial def Lean.CollectLevelMVars.collect : Level → Visitor

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

partial def Lean.CollectLevelMVars.main : Expr → Visitor

def Lean.collectLevelMVars (s : CollectLevelMVars.State) (e : Expr) : 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