summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon HO2024-03-18 07:23:00 +0100
committerGitHub2024-03-18 07:23:00 +0100
commita24f42ff7f0ae3c2aeb51decb0d0c90d6e50ffac (patch)
tree7c9e526912d4fcbde4ed2ff4c17988fd5c89c96e /tests/coq/misc
parentd56946242859e0d375c1d44585b9da6d5fbe94cb (diff)
parent9e230d0c4378b5c992c820cc1f4322896f739095 (diff)
Merge pull request #92 from AeneasVerif/son/globals
Add generics to constants/globals
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Constants.v17
1 files changed, 17 insertions, 0 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 5fa952b4..fcafed53 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -158,4 +158,21 @@ Definition s3 : Pair_t u32 u32 := s3_body%global.
Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
Definition s4 : Pair_t u32 u32 := s4_body%global.
+(** [constants::V]
+ Source: 'src/constants.rs', lines 86:0-86:31 *)
+Record V_t (T : Type) (N : usize) := mkV_t { v_x : array T N; }.
+
+Arguments mkV_t { _ _ }.
+Arguments v_x { _ _ }.
+
+(** [constants::{constants::V<T, N>#1}::LEN]
+ Source: 'src/constants.rs', lines 91:4-91:24 *)
+Definition v_len_body (T : Type) (N : usize) : result usize := Return N.
+Definition v_len (T : Type) (N : usize) : usize := (v_len_body T N)%global.
+
+(** [constants::use_v]:
+ Source: 'src/constants.rs', lines 94:0-94:42 *)
+Definition use_v (T : Type) (N : usize) : result usize :=
+ Return (v_len T N).
+
End Constants.