diff --git a/doc/changelog/06-Ltac2-language/22264-ltac2-constr-sort-predicates-Added.rst b/doc/changelog/06-Ltac2-language/22264-ltac2-constr-sort-predicates-Added.rst new file mode 100644 index 000000000000..5e2c180fbc46 --- /dev/null +++ b/doc/changelog/06-Ltac2-language/22264-ltac2-constr-sort-predicates-Added.rst @@ -0,0 +1,4 @@ +- **Added:** + Ltac2 functions ``Constr.is_prop``, ``Constr.is_set``, ``Constr.is_sprop``, ``Constr.is_type`` and ``Constr.is_type_or_set`` + (`#22264 `_, + by Jason Gross). diff --git a/test-suite/ltac2/constr_sort_predicates.v b/test-suite/ltac2/constr_sort_predicates.v new file mode 100644 index 000000000000..413a21d3a4cc --- /dev/null +++ b/test-suite/ltac2/constr_sort_predicates.v @@ -0,0 +1,21 @@ +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_prop constr:(Prop)). +Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(Set))). +Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(Type))). +Ltac2 Eval check (Constr.is_set constr:(Set)). +Ltac2 Eval check (Bool.neg (Constr.is_set constr:(Prop))). +Ltac2 Eval check (Constr.is_sprop constr:(SProp)). +Ltac2 Eval check (Bool.neg (Constr.is_sprop constr:(Prop))). +Ltac2 Eval check (Constr.is_type constr:(Type)). +Ltac2 Eval check (Bool.neg (Constr.is_type constr:(Prop))). +Ltac2 Eval check (Bool.neg (Constr.is_type constr:(Set))). +Ltac2 Eval check (Bool.neg (Constr.is_type constr:(SProp))). +Ltac2 Eval check (Bool.neg (Constr.is_type constr:(nat))). +Ltac2 Eval check (Constr.is_type_or_set constr:(Set)). +Ltac2 Eval check (Constr.is_type_or_set constr:(Type)). +Ltac2 Eval check (Bool.neg (Constr.is_type_or_set constr:(Prop))). +Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(0))). diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v index ce39400e7082..d029255e206d 100644 --- a/theories/Ltac2/Constr.v +++ b/theories/Ltac2/Constr.v @@ -600,3 +600,27 @@ Ltac2 is_sort(c: constr) := | Unsafe.Sort _ => true | _ => false end. + +(** [is_prop c] returns [true] iff [c] is the sort [Prop]. *) +Ltac2 is_prop (c : constr) : bool := equal c constr:(Prop). + +(** [is_set c] returns [true] iff [c] is the sort [Set]. *) +Ltac2 is_set (c : constr) : bool := equal c constr:(Set). + +(** [is_sprop c] returns [true] iff [c] is the sort [SProp]. *) +Ltac2 is_sprop (c : constr) : bool := equal c constr:(SProp). + +(** [is_type c] returns [true] iff [c] is a sort of the form + [Type@{u}], i.e. a sort other than [Prop], [Set] and [SProp]. *) +Ltac2 is_type (c : constr) : bool := + if is_sort c + then if is_prop c then false + else if is_set c then false + else if is_sprop c then false + else true + else false. + +(** [is_type_or_set c] returns [true] iff [c] is [Set] or a sort of + the form [Type@{u}]. *) +Ltac2 is_type_or_set (c : constr) : bool := + if is_type c then true else is_set c.