@[inline, reducible]

abbrev Lean.FindMVar.Visitor : Type

Equations

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

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

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

@[inline]

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

Equations

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