@[reducible, inline]

abbrev Lean.FindLevelMVar.Visitor : Type

partial def Lean.FindLevelMVar.visit (p : Lean.LMVarId → Bool) (e : Lean.Expr) : Lean.FindLevelMVar.Visitor

partial def Lean.FindLevelMVar.main (p : Lean.LMVarId → Bool) : Lean.Expr → Lean.FindLevelMVar.Visitor

partial def Lean.FindLevelMVar.visitLevel (p : Lean.LMVarId → Bool) (l : Lean.Level) : Lean.FindLevelMVar.Visitor

partial def Lean.FindLevelMVar.mainLevel (p : Lean.LMVarId → Bool) : Lean.Level → Lean.FindLevelMVar.Visitor

@[inline]

def Lean.Expr.findLevelMVar? (e : Lean.Expr) (p : Lean.LMVarId → Bool) : Option Lean.LMVarId

Equations

• e.findLevelMVar? p = Lean.FindLevelMVar.main p e none