@[reducible, inline]

abbrev Lean.FindMVar.Visitor : Type

Equations

• Lean.FindMVar.Visitor = (Option Lean.MVarId → Option Lean.MVarId)

partial def Lean.FindMVar.visit (p : MVarId → Bool) (e : Expr) : Visitor

partial def Lean.FindMVar.main (p : MVarId → Bool) : Expr → Visitor

@[inline]

def Lean.Expr.findMVar? (e : Expr) (p : MVarId → Bool) : Option MVarId

Equations

• e.findMVar? p = Lean.FindMVar.main p e none