@[extern lean_find_expr]

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

@[inline]

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

Equations

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

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

Returns 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

Returns type for findExt? function argument.

• found : FindStep

  Found desired subterm

• visit : FindStep

  Search subterms

• done : FindStep

  Do not search subterms

@[extern lean_find_ext_expr]

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

@[inline]

def Lean.Expr.findExt? (p : Expr → FindStep) (e : Expr) : Option 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