summaryrefslogtreecommitdiff
path: root/backends/coq
diff options
context:
space:
mode:
authorSon Ho2023-09-07 16:02:43 +0200
committerSon Ho2023-09-07 16:02:43 +0200
commit1181aecddbcb3232c21b191fbde59c2e9596846a (patch)
treed246e01bb874f44ae6e10164ee357f1fbb6caf11 /backends/coq
parent8b18c0da053e069b5a2d9fbf06f45eae2f05a029 (diff)
Fix some issues
Diffstat (limited to '')
-rw-r--r--backends/coq/Primitives.v14
1 files changed, 14 insertions, 0 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;