Add Ltac2 Constr.is_rel, is_meta, is_cast, is_prod, is_lambda, is_letin, is_app and is_case

doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 functions ``Constr.is_rel``, ``Constr.is_meta``, ``Constr.is_cast``, ``Constr.is_prod``, ``Constr.is_lambda``, ``Constr.is_letin``, ``Constr.is_app`` and ``Constr.is_case``
+  (`#22260 <https://github.com/rocq-prover/rocq/pull/22260>`_,
+  by Jason Gross).

test-suite/ltac2/constr_is_kind.v

@@ -0,0 +1,20 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure.
+
+Ltac2 Eval check (Constr.is_prod constr:(nat -> nat)).
+Ltac2 Eval check (Constr.is_prod constr:(forall n : nat, n = n)).
+Ltac2 Eval check (Bool.neg (Constr.is_prod constr:(fun n : nat => n))).
+Ltac2 Eval check (Constr.is_lambda constr:(fun n : nat => n)).
+Ltac2 Eval check (Bool.neg (Constr.is_lambda constr:(nat -> nat))).
+Ltac2 Eval check (Constr.is_letin constr:(let x := 1 in x)).
+Ltac2 Eval check (Bool.neg (Constr.is_letin constr:(S 0))).
+Ltac2 Eval check (Constr.is_app constr:(S 0)).
+Ltac2 Eval check (Bool.neg (Constr.is_app constr:(S))).
+Ltac2 Eval check (Constr.is_case constr:(match 0 with 0 => 0 | S n => n end)).
+Ltac2 Eval check (Bool.neg (Constr.is_case constr:(S 0))).
+Ltac2 Eval check (Constr.is_rel (Constr.Unsafe.make (Constr.Unsafe.Rel 1))).
+Ltac2 Eval check (Bool.neg (Constr.is_rel constr:(0))).
+Ltac2 Eval check (Bool.neg (Constr.is_meta constr:(0))).
+Ltac2 Eval check (Bool.neg (Constr.is_cast constr:(S 0))).

theories/Ltac2/Constr.v

@@ -600,3 +600,51 @@ Ltac2 is_sort(c: constr) :=
   | Unsafe.Sort _ => true
   | _ => false
   end.
+
+Ltac2 is_rel(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Rel _ => true
+  | _ => false
+  end.
+
+Ltac2 is_meta(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Meta _ => true
+  | _ => false
+  end.
+
+Ltac2 is_cast(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Cast _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_prod(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Prod _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_lambda(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Lambda _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_letin(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.LetIn _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_app(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.App _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_case(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Case _ _ _ _ _ => true
+  | _ => false
+  end.