@[inline]
Instances For
Instances For
Instances For
@[implemented_by Lean.Expr.FindImpl.findUnsafe?]
Equations
- One or more equations did not get rendered due to their size.
- Lean.Expr.find? p (Lean.Expr.mdata data b) = if p (Lean.Expr.mdata data b) = true then some (Lean.Expr.mdata data b) else Lean.Expr.find? p b
- Lean.Expr.find? p (Lean.Expr.app f a) = if p (Lean.Expr.app f a) = true then some (Lean.Expr.app f a) else HOrElse.hOrElse (Lean.Expr.find? p f) fun x => Lean.Expr.find? p a
- Lean.Expr.find? p (Lean.Expr.proj typeName idx b) = if p (Lean.Expr.proj typeName idx b) = true then some (Lean.Expr.proj typeName idx b) else Lean.Expr.find? p b
- Lean.Expr.find? p e = if p e = true then some e else none
Instances For
Return true if e
occurs in t
Instances For
- found: Lean.Expr.FindStep
Found desired subterm
- visit: Lean.Expr.FindStep
Search subterms
- done: Lean.Expr.FindStep
Do not search subterms
Return type for findExt?
function argument.
Instances For
Instances For
unsafe def
Lean.Expr.FindExtImpl.findM?.visitApp
(p : Lean.Expr → Lean.Expr.FindStep)
(e : Lean.Expr)
:
Instances For
unsafe def
Lean.Expr.FindExtImpl.findM?.visit
(p : Lean.Expr → Lean.Expr.FindStep)
(e : Lean.Expr)
:
Instances For
Instances For
@[implemented_by Lean.Expr.FindExtImpl.findUnsafe?]
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.