summaryrefslogtreecommitdiff
path: root/tests/fstar/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/fstar/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/fstar/misc/Constants.fst14
1 files changed, 14 insertions, 0 deletions
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 66429c80..8d1cf3ce 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -143,3 +143,17 @@ let s3 : pair_t u32 u32 = eval_global s3_body
let s4_body : result (pair_t u32 u32) = mk_pair1 7 8
let s4 : pair_t u32 u32 = eval_global s4_body
+(** [constants::V]
+ Source: 'src/constants.rs', lines 86:0-86:31 *)
+type v_t (t : Type0) (n : usize) = { x : array t n; }
+
+(** [constants::{constants::V<T, N>#1}::LEN]
+ Source: 'src/constants.rs', lines 91:4-91:24 *)
+let v_len_body (t : Type0) (n : usize) : result usize = Return n
+let v_len (t : Type0) (n : usize) : usize = eval_global (v_len_body t n)
+
+(** [constants::use_v]:
+ Source: 'src/constants.rs', lines 94:0-94:42 *)
+let use_v (t : Type0) (n : usize) : result usize =
+ Return (v_len t n)
+