diff options
author | Aymeric Fromherz | 2024-05-24 15:02:26 +0200 |
---|---|---|
committer | Aymeric Fromherz | 2024-05-24 15:02:26 +0200 |
commit | 4d33ea68ca1ebfca35b7d7332f63b74dd3c06838 (patch) | |
tree | 838da53ae7e5be27e1dde684d0354a5ce2a1fd99 /tests/fstar/misc/Paper.fst | |
parent | ac5f261997079002a782217ebf0c854e31bb880d (diff) | |
parent | 3c8ea6df20f92be9c341bbfb748f65d6c598fead (diff) |
Merge remote-tracking branch 'origin/main' into afromher_debug
Diffstat (limited to 'tests/fstar/misc/Paper.fst')
-rw-r--r-- | tests/fstar/misc/Paper.fst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index e6b4eb25..2e74e21a 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -6,12 +6,12 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [paper::ref_incr]: - Source: 'src/paper.rs', lines 4:0-4:28 *) + Source: 'tests/src/paper.rs', lines 4:0-4:28 *) let ref_incr (x : i32) : result i32 = i32_add x 1 (** [paper::test_incr]: - Source: 'src/paper.rs', lines 8:0-8:18 *) + Source: 'tests/src/paper.rs', lines 8:0-8:18 *) let test_incr : result unit = let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Ok () @@ -19,7 +19,7 @@ let test_incr : result unit = let _ = assert_norm (test_incr = Ok ()) (** [paper::choose]: - Source: 'src/paper.rs', lines 15:0-15:70 *) + Source: 'tests/src/paper.rs', lines 15:0-15:70 *) let choose (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = if b @@ -27,7 +27,7 @@ let choose else let back = fun ret -> Ok (x, ret) in Ok (y, back) (** [paper::test_choose]: - Source: 'src/paper.rs', lines 23:0-23:20 *) + Source: 'tests/src/paper.rs', lines 23:0-23:20 *) let test_choose : result unit = let* (z, choose_back) = choose i32 true 0 0 in let* z1 = i32_add z 1 in @@ -43,13 +43,13 @@ let test_choose : result unit = let _ = assert_norm (test_choose = Ok ()) (** [paper::List] - Source: 'src/paper.rs', lines 35:0-35:16 *) + Source: 'tests/src/paper.rs', lines 35:0-35:16 *) type list_t (t : Type0) = | List_Cons : t -> list_t t -> list_t t | List_Nil : list_t t (** [paper::list_nth_mut]: - Source: 'src/paper.rs', lines 42:0-42:67 *) + Source: 'tests/src/paper.rs', lines 42:0-42:67 *) let rec list_nth_mut (t : Type0) (l : list_t t) (i : u32) : result (t & (t -> result (list_t t))) @@ -68,7 +68,7 @@ let rec list_nth_mut end (** [paper::sum]: - Source: 'src/paper.rs', lines 57:0-57:32 *) + Source: 'tests/src/paper.rs', lines 57:0-57:32 *) let rec sum (l : list_t i32) : result i32 = begin match l with | List_Cons x tl -> let* i = sum tl in i32_add x i @@ -76,7 +76,7 @@ let rec sum (l : list_t i32) : result i32 = end (** [paper::test_nth]: - Source: 'src/paper.rs', lines 68:0-68:17 *) + Source: 'tests/src/paper.rs', lines 68:0-68:17 *) let test_nth : result unit = let l = List_Cons 3 List_Nil in let l1 = List_Cons 2 l in @@ -90,7 +90,7 @@ let test_nth : result unit = let _ = assert_norm (test_nth = Ok ()) (** [paper::call_choose]: - Source: 'src/paper.rs', lines 76:0-76:44 *) + Source: 'tests/src/paper.rs', lines 76:0-76:44 *) let call_choose (p : (u32 & u32)) : result u32 = let (px, py) = p in let* (pz, choose_back) = choose u32 true px py in |