structure Lean.CollectLevelMVars.State : Type

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

instance Lean.CollectLevelMVars.instInhabitedState : Inhabited State

@[reducible, inline]

abbrev Lean.CollectLevelMVars.Visitor : Type

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.