@[extern lean_find_expr]

opaque Lean.Expr.findImpl? (p : Lean.Expr → Bool) (e : Lean.Expr) : Option Lean.Expr

@[inline]

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

Equations

• Lean.Expr.find? p e = Lean.Expr.findImpl? p e

def Lean.Expr.occurs (e t : Lean.Expr) : Bool

Return true if e occurs in t

Equations

• e.occurs t = (Lean.Expr.find? (fun (s : Lean.Expr) => s == e) t).isSome

inductive Lean.Expr.FindStep : Type

Return type for findExt? function argument.

• found: Lean.Expr.FindStep

  Found desired subterm

• visit: Lean.Expr.FindStep

  Search subterms

• done: Lean.Expr.FindStep

  Do not search subterms

@[extern lean_find_ext_expr]

opaque Lean.Expr.findExtImpl? (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : Option Lean.Expr

@[inline]

def Lean.Expr.findExt? (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : Option Lean.Expr

Similar to find?, but p can return FindStep.done to interrupt the search on subterms. Remark: Differently from find?, we do not invoke p for partial applications of an application.

Equations

• Lean.Expr.findExt? p e = Lean.Expr.findExtImpl? p e