From dfce2ae74d20ebe7dc9d90051307464dc2a3baf0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Wed, 8 Jul 2026 18:14:34 +0000
Subject: [PATCH] Add Ltac2 Constr.is_rel, is_meta, is_cast, is_prod,
 is_lambda, is_letin, is_app and is_case

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
---
 .../22260-ltac2-constr-is-kind-Added.rst      |  4 ++
 test-suite/ltac2/constr_is_kind.v             | 20 ++++++++
 theories/Ltac2/Constr.v                       | 48 +++++++++++++++++++
 3 files changed, 72 insertions(+)
 create mode 100644 doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst
 create mode 100644 test-suite/ltac2/constr_is_kind.v

diff --git a/doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst b/doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst
new file mode 100644
index 000000000000..4f18a15bcdde
--- /dev/null
+++ b/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).
diff --git a/test-suite/ltac2/constr_is_kind.v b/test-suite/ltac2/constr_is_kind.v
new file mode 100644
index 000000000000..9fabadc4dbf2
--- /dev/null
+++ b/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))).
diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v
index ce39400e7082..bae4c954caa0 100644
--- a/theories/Ltac2/Constr.v
+++ b/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.