Merge PR #11948: Hexadecimal numerals

Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin

1 files changed, 46 insertions, 31 deletions

diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 36fc1a5914..13d0a9e55b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,47 +1,61 @@
 false: bool
 true: bool
 negb: bool -> bool
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
-andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-Nat.even: nat -> bool
+andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 Nat.odd: nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+Hexadecimal.hexadecimal_beq:
+  Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool
+Numeral.int_beq: Numeral.int -> Numeral.int -> bool
+Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
+Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
+Decimal.int_beq: Decimal.int -> Decimal.int -> bool
+Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 (use "About" for full details on implicit arguments)
 Nat.two: nat
-Nat.one: nat
 Nat.zero: nat
+Nat.one: nat
 O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
 Nat.div2: nat -> nat
 Nat.log2: nat -> nat
-Nat.succ: nat -> nat
-Nat.sqrt: nat -> nat
-S: nat -> nat
 Nat.pred: nat -> nat
-Nat.double: nat -> nat
 Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.tail_mul: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.pow: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Hexadecimal.nb_digits: Hexadecimal.uint -> nat
+Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.of_num_uint: Numeral.uint -> nat
 Nat.of_uint: Decimal.uint -> nat
 Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
@@ -53,29 +67,30 @@ Nat.div2: nat -> nat
 Nat.sqrt: nat -> nat
 Nat.log2: nat -> nat
 Nat.double: nat -> nat
-Nat.pred: nat -> nat
+S: nat -> nat
 Nat.square: nat -> nat
 Nat.succ: nat -> nat
-S: nat -> nat
+Nat.pred: nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.pow: nat -> nat -> nat
-Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
-Nat.tail_mul: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
+Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 (use "About" for full details on implicit arguments)
 mult_n_Sm: forall n m : nat, n * m + n = n * S m