diff --git a/doc/changelog/06-Ltac2-language/17894-is_float.rst b/doc/changelog/06-Ltac2-language/17894-is_float.rst new file mode 100644 index 000000000000..fe10bb89e737 --- /dev/null +++ b/doc/changelog/06-Ltac2-language/17894-is_float.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Ltac2.Constr.is_float``, ``Ltac2.Constr.is_uint63``, ``Ltac2.Constr.is_array`` + (`#17894 `_, + by Jason Gross). diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 451b2d91c460..df6a4af8ef1a 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -190,3 +190,21 @@ Ltac2 is_const(c: constr) := | Unsafe.Constant _ _ => true | _ => false end. + +Ltac2 is_float(c: constr) := + match Unsafe.kind c with + | Unsafe.Float _ => true + | _ => false + end. + +Ltac2 is_uint63(c: constr) := + match Unsafe.kind c with + | Unsafe.Uint63 _ => true + | _ => false + end. + +Ltac2 is_array(c: constr) := + match Unsafe.kind c with + | Unsafe.Array _ _ _ _ => true + | _ => false + end.