From 62574f76016d54ef791cd8f355192b91034dd18d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 25 Nov 2024 16:46:14 +0100 Subject: [PATCH] Ltac2: add Char.of_int_opt --- .../06-Ltac2-language/19873-ltac2-char-int-opt.rst | 4 ++++ user-contrib/Ltac2/Char.v | 7 ++++++- 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/06-Ltac2-language/19873-ltac2-char-int-opt.rst 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 new file mode 100644 index 000000000000..9c71ae591483 --- /dev/null +++ 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 `_, + by Gaëtan Gilbert). diff --git a/user-contrib/Ltac2/Char.v b/user-contrib/Ltac2/Char.v index 437344554961..d8a84cf01e41 100644 --- 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).