Documentation

Lean.Util.FindExpr

source
@[extern lean_find_expr]
opaque Lean.Expr.findImpl? (p : Expr → Bool) (e : Expr) :
Option Expr
source
@[inline]
def Lean.Expr.find? (p : Expr → Bool) (e : Expr) :
Option Expr
Equations
    Instances For
      source
      def Lean.Expr.occurs (e t : Expr) :
      Bool

      Returns true if e occurs in t

      Equations
        Instances For
          source
          inductive Lean.Expr.FindStep :
          Type

          Returns type for findExt? function argument.

          Instances For
            source
            @[extern lean_find_ext_expr]
            opaque Lean.Expr.findExtImpl? (p : Expr → FindStep) (e : Expr) :
            Option Expr
            source
            @[inline]
            def Lean.Expr.findExt? (p : Expr → FindStep) (e : Expr) :
            Option 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.

            Equations
              Instances For