Ltac2: add Char.of_int_opt

SkySkimmer · Dec 18, 2024 · 62574f7 · 62574f7
1 parent eafed8f
commit 62574f7
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/doc/changelog/06-Ltac2-language/19873-ltac2-char-int-opt.rst b/doc/changelog/06-Ltac2-language/19873-ltac2-char-int-opt.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  `Ltac2.Char.of_int_opt` returning `None` on invalid integers
+  (`#19873 <https://github.com/coq/coq/pull/19873>`_,
+  by Gaëtan Gilbert).
diff --git a/user-contrib/Ltac2/Char.v b/user-contrib/Ltac2/Char.v
@@ -9,11 +9,16 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
-Require Ltac2.Int.
+Require Ltac2.Int Ltac2.Control.
 
 Ltac2 @external of_int : int -> char := "rocq-runtime.plugins.ltac2" "char_of_int".
 (** Throws if the integer is not a valid char (in range [0-255]). *)
 
+Ltac2 of_int_opt (x:int) : char option :=
+  if Int.lt x 0 then None
+  else if Int.lt 255 x then None
+  else Some (of_int x).
+
 Ltac2 @external to_int : char -> int := "rocq-runtime.plugins.ltac2" "char_to_int".
 
 Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y).