@[reducible, inline]

unsafe abbrev Lean.Expr.FindImpl.FindM (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• Lean.Expr.FindImpl.FindM m = StateT (Lean.PtrSet Lean.Expr) m

@[inline]

unsafe def Lean.Expr.FindImpl.checkVisited {m : Type → Type u_1} [Monad m] (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM m) Unit

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FindImpl.findM? {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM m) Lean.Expr

Equations

• Lean.Expr.FindImpl.findM? p e = Lean.Expr.FindImpl.findM?.visit p e

unsafe def Lean.Expr.FindImpl.findM?.visit {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM m) Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FindImpl.findUnsafeM? {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) (e : Lean.Expr) : m (Option Lean.Expr)

Equations

• Lean.Expr.FindImpl.findUnsafeM? p e = StateT.run' (Lean.Expr.FindImpl.findM? p e) Lean.mkPtrSet

@[inline]

unsafe def Lean.Expr.FindImpl.findUnsafe? (p : Lean.Expr → Bool) (e : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Expr.FindImpl.findUnsafe? p e = Lean.Expr.FindImpl.findUnsafeM? p e

@[implemented_by Lean.Expr.FindImpl.findUnsafeM?]

def Lean.Expr.findM? {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) (e : Lean.Expr) : m (Option Lean.Expr)

@[implemented_by Lean.Expr.FindImpl.findUnsafe?]

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

Equations

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

def Lean.Expr.occurs (e : Lean.Expr) (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

unsafe def Lean.Expr.FindExtImpl.findM? (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM Id) Lean.Expr

Equations

• Lean.Expr.FindExtImpl.findM? p e = Lean.Expr.FindExtImpl.findM?.visit p e

unsafe def Lean.Expr.FindExtImpl.findM?.visitApp (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM Id) Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FindExtImpl.findM?.visit (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : OptionT (Lean.Expr.FindImpl.FindM Id) Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FindExtImpl.findUnsafe? (p : Lean.Expr → Lean.Expr.FindStep) (e : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Expr.FindExtImpl.findUnsafe? p e = (StateT.run' (Lean.Expr.FindExtImpl.findM? p e) Lean.mkPtrSet).run

@[implemented_by Lean.Expr.FindExtImpl.findUnsafe?]

opaque 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.