@[inline, reducible]
unsafe abbrev Lean.Expr.FindImpl.FindM (α : Type) :
Instances For
    @[implemented_by Lean.Expr.FindImpl.findUnsafe?]
    Instances For

      Return true if e occurs in t

      Instances For

        Return type for findExt? function argument.

        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.