source
structure Lean.CollectLevelMVars.State :
Type

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

Instances For

source
instance Lean.CollectLevelMVars.instInhabitedState :
Inhabited State
Equations

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

source
@[reducible, inline]
abbrev Lean.CollectLevelMVars.Visitor :
Type
Equations

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

Instances For

source
partial def Lean.CollectLevelMVars.visitLevel (u : Level) :
Visitor
source
partial def Lean.CollectLevelMVars.collect :
Level → Visitor
source
partial def Lean.CollectLevelMVars.visitExpr (e : Expr) :
Visitor
source
partial def Lean.CollectLevelMVars.main :
Expr → Visitor
source
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

Instances For