@[reducible, inline]
Equations
Instances For
@[inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Expr.FindImpl.findUnsafe? p e = (StateT.run' (Lean.Expr.FindImpl.findM? p e) Lean.mkPtrSet).run
Instances For
Return true if e
occurs in t
Equations
- e.occurs t = (Lean.Expr.find? (fun (s : Lean.Expr) => s == e) t).isSome
Instances For
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
Instances For
Equations
Instances For
unsafe def
Lean.Expr.FindExtImpl.findM?.visitApp
(p : Lean.Expr → Lean.Expr.FindStep)
(e : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
unsafe def
Lean.Expr.FindExtImpl.findM?.visit
(p : Lean.Expr → Lean.Expr.FindStep)
(e : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Expr.FindExtImpl.findUnsafe? p e = (StateT.run' (Lean.Expr.FindExtImpl.findM? p e) Lean.mkPtrSet).run
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.