Documentation

Lean.Meta.CtorRecognizer

source
def Lean.Meta.isConstructorAppCore? (e : Expr) :
MetaM (Option ConstructorVal)

If e is a constructor application, then return the corresponding ConstructorVal.

Instances For
    source
    def Lean.Meta.isConstructorApp? (e : Expr) :
    MetaM (Option ConstructorVal)

    If e is a constructor application or a builtin literal defeq to a constructor application, then return the corresponding ConstructorVal.

    Instances For
      source
      def Lean.Meta.isConstructorApp'? (e : Expr) :
      MetaM (Option ConstructorVal)

      Similar to isConstructorApp?, but uses whnf. It also uses isOffset? for Nat.

      See also Lean.Meta.constructorApp'?.

      Instances For
        source
        def Lean.Meta.isConstructorApp (e : Expr) :
        MetaM Bool

        Returns true, if e is constructor application of builtin literal defeq to a constructor application.

        Instances For
          source
          def Lean.Meta.isConstructorApp' (e : Expr) :
          MetaM Bool

          Returns true if isConstructorApp e or isConstructorApp (← whnf e)

          Instances For
            source
            def Lean.Meta.constructorApp? (e : Expr) :
            MetaM (Option (ConstructorVal × Array Expr))

            If e is a constructor application, return a pair containing the corresponding ConstructorVal and the constructor application arguments.

            Instances For
              source
              def Lean.Meta.constructorApp'? (e : Expr) :
              MetaM (Option (ConstructorVal × Array Expr))

              Similar to constructorApp?, but on failure it puts e in WHNF and tries again. It also uses isOffset? for Nat.

              See also Lean.Meta.isConstructorApp'?.

              Instances For