feat: add little-endian numeral notation conversions for positive, N, Z

theories/NArith/BinNatDef.v

@@ -342,6 +342,32 @@ Definition to_num_int n := Number.IntDecimal (to_int n).
 
 Definition to_num_hex_int n := Number.IntHexadecimal (to_hex_int n).
 
+(** ** Little-endian conversions (least significant digit first) *)
+
+Definition of_luint (d:Decimal.luint) := Pos.of_luint d.
+Definition of_hex_luint (d:Hexadecimal.luint) := Pos.of_hex_luint d.
+
+Definition of_num_luint (d:Number.luint) :=
+  match d with
+  | Number.LUIntDecimal d => of_luint d
+  | Number.LUIntHexadecimal d => of_hex_luint d
+  end.
+
+Definition to_luint n :=
+  match n with
+  | 0 => {| Decimal.luint_IsLittleEndian := Decimal.zero |}
+  | pos p => Pos.to_luint p
+  end.
+
+Definition to_hex_luint n :=
+  match n with
+  | 0 => {| Hexadecimal.luint_IsLittleEndian := Hexadecimal.zero |}
+  | pos p => Pos.to_hex_luint p
+  end.
+
+Definition to_num_luint n := Number.LUIntDecimal (to_luint n).
+Definition to_num_hex_luint n := Number.LUIntHexadecimal (to_hex_luint n).
+
 Number Notation N of_num_uint to_num_hex_uint : hex_N_scope.
 Number Notation N of_num_uint to_num_uint : N_scope.
 

theories/PArith/BinPosDef.v

@@ -375,6 +375,56 @@ Definition to_num_int n := Number.IntDecimal (to_int n).
 
 Definition to_num_hex_int n := Number.IntHexadecimal (to_hex_int n).
 
+(** ** Little-endian conversions (least significant digit first) *)
+
+Definition of_luint (d:Decimal.luint) :=
+  of_uint (Decimal.rev (Decimal.luint_IsLittleEndian d)).
+
+Definition of_hex_luint (d:Hexadecimal.luint) :=
+  of_hex_uint (Hexadecimal.rev (Hexadecimal.luint_IsLittleEndian d)).
+
+Definition of_num_luint (d:Number.luint) : N :=
+  match d with
+  | Number.LUIntDecimal d => of_luint d
+  | Number.LUIntHexadecimal d => of_hex_luint d
+  end.
+
+Definition of_lint (d:Decimal.lint) : option positive :=
+  of_int (match Decimal.lint_IsLittleEndian d with
+          | Decimal.Pos u => Decimal.Pos (Decimal.rev u)
+          | Decimal.Neg u => Decimal.Neg (Decimal.rev u)
+          end).
+
+Definition of_hex_lint (d:Hexadecimal.lint) : option positive :=
+  of_hex_int (match Hexadecimal.lint_IsLittleEndian d with
+              | Hexadecimal.Pos u => Hexadecimal.Pos (Hexadecimal.rev u)
+              | Hexadecimal.Neg u => Hexadecimal.Neg (Hexadecimal.rev u)
+              end).
+
+Definition of_num_lint (d:Number.lint) : option positive :=
+  match d with
+  | Number.LIntDecimal d => of_lint d
+  | Number.LIntHexadecimal d => of_hex_lint d
+  end.
+
+Definition to_luint p :=
+  {| Decimal.luint_IsLittleEndian := to_little_uint p |}.
+
+Definition to_hex_luint p :=
+  {| Hexadecimal.luint_IsLittleEndian := to_little_hex_uint p |}.
+
+Definition to_num_luint p := Number.LUIntDecimal (to_luint p).
+Definition to_num_hex_luint p := Number.LUIntHexadecimal (to_hex_luint p).
+
+Definition to_lint n :=
+  {| Decimal.lint_IsLittleEndian := Decimal.Pos (to_little_uint n) |}.
+
+Definition to_hex_lint p :=
+  {| Hexadecimal.lint_IsLittleEndian := Hexadecimal.Pos (to_little_hex_uint p) |}.
+
+Definition to_num_lint n := Number.LIntDecimal (to_lint n).
+Definition to_num_hex_lint n := Number.LIntHexadecimal (to_hex_lint n).
+
 Number Notation positive of_num_int to_num_hex_uint : hex_positive_scope.
 Number Notation positive of_num_int to_num_uint : positive_scope.
 

theories/ZArith/BinIntDef.v

@@ -304,6 +304,48 @@ Definition ldiff a b :=
    | neg a, neg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a))
  end.
 
+(** ** Little-endian conversions (least significant digit first) *)
+
+Definition of_luint (d:Decimal.luint) := of_N (Pos.of_luint d).
+Definition of_hex_luint (d:Hexadecimal.luint) := of_N (Pos.of_hex_luint d).
+
+Definition of_lint (d:Decimal.lint) :=
+  of_int (match Decimal.lint_IsLittleEndian d with
+          | Decimal.Pos u => Decimal.Pos (Decimal.rev u)
+          | Decimal.Neg u => Decimal.Neg (Decimal.rev u)
+          end).
+
+Definition of_hex_lint (d:Hexadecimal.lint) :=
+  of_hex_int (match Hexadecimal.lint_IsLittleEndian d with
+              | Hexadecimal.Pos u => Hexadecimal.Pos (Hexadecimal.rev u)
+              | Hexadecimal.Neg u => Hexadecimal.Neg (Hexadecimal.rev u)
+              end).
+
+Definition of_num_lint (d:Number.lint) :=
+  match d with
+  | Number.LIntDecimal d => of_lint d
+  | Number.LIntHexadecimal d => of_hex_lint d
+  end.
+
+Definition to_lint n :=
+  {| Decimal.lint_IsLittleEndian :=
+    match n with
+    | 0 => Decimal.Pos Decimal.zero
+    | pos p => Decimal.Pos (Pos.to_little_uint p)
+    | neg p => Decimal.Neg (Pos.to_little_uint p)
+    end |}.
+
+Definition to_hex_lint n :=
+  {| Hexadecimal.lint_IsLittleEndian :=
+    match n with
+    | 0 => Hexadecimal.Pos Hexadecimal.zero
+    | pos p => Hexadecimal.Pos (Pos.to_little_hex_uint p)
+    | neg p => Hexadecimal.Neg (Pos.to_little_hex_uint p)
+    end |}.
+
+Definition to_num_lint n := Number.LIntDecimal (to_lint n).
+Definition to_num_hex_lint n := Number.LIntHexadecimal (to_hex_lint n).
+
 Number Notation Z of_num_int to_num_hex_int : hex_Z_scope.
 Number Notation Z of_num_int to_num_int : Z_scope.