@[inline, reducible]

abbrev Lean.FindLevelMVar.Visitor : Type

Equations

• Lean.FindLevelMVar.Visitor = (Option Lean.LMVarId → Option Lean.LMVarId)

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

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