Documentation

Lean.Util.FindExpr

@[inline]

abbrev Lean.Expr.FindImpl.cacheSize:

Equations

Lean.Expr.FindImpl.cacheSize = 8192

structure Lean.Expr.FindImpl.State:

Type

keys : Array Lean.Expr

@[inline]

abbrev Lean.Expr.FindImpl.FindM (α : Type) :

Type

Equations

Lean.Expr.FindImpl.FindM = StateT Lean.Expr.FindImpl.State Id

unsafe def Lean.Expr.FindImpl.visited (e : Lean.Expr) (size : USize) :

Lean.Expr.FindImpl.FindM Bool

Equations

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

unsafe def Lean.Expr.FindImpl.findM? (p : Lean.Expr → Bool) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM Lean.Expr

Equations

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

unsafe def Lean.Expr.FindImpl.findM?.visit (p : Lean.Expr → Bool) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM Lean.Expr

Equations

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

unsafe def Lean.Expr.FindImpl.initCache:

Lean.Expr.FindImpl.State

Equations

Lean.Expr.FindImpl.initCache = { keys := mkArray (USize.toNat Lean.Expr.FindImpl.cacheSize) (cast Lean.Expr.FindImpl.initCache.proof_1 ()) }

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

Option Lean.Expr

Equations

Lean.Expr.FindImpl.findUnsafe? p e = Id.run (StateT.run' (Lean.Expr.FindImpl.findM? p Lean.Expr.FindImpl.cacheSize e) Lean.Expr.FindImpl.initCache)

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

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

Option Lean.Expr

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

Return true if e occurs in t

Equations

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

inductive Lean.Expr.FindStep:

Type

Return type for findExt? function argument.

unsafe def Lean.Expr.FindExtImpl.findM? (p : Lean.Expr → Lean.Expr.FindStep) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM Lean.Expr

Equations

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

unsafe def Lean.Expr.FindExtImpl.findM?.visitApp (p : Lean.Expr → Lean.Expr.FindStep) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM 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) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM 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 = Id.run (StateT.run' (Lean.Expr.FindExtImpl.findM? p Lean.Expr.FindImpl.cacheSize e) Lean.Expr.FindImpl.initCache)

@[implementedBy 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.