diff options
author | Son HO | 2024-06-11 14:36:40 +0200 |
---|---|---|
committer | GitHub | 2024-06-11 14:36:40 +0200 |
commit | e60d525fe3dffa035d2a551af624747dca6e1c1e (patch) | |
tree | d7b06e270fd6a1cf69717f98db7c30e43788dad1 /tests/fstar | |
parent | 73e27b142b65ec37fbbc55a5a7d0299555b2b60b (diff) | |
parent | 2e91b90e332c473253c2ff91fd65da34eb709572 (diff) |
Merge pull request #237 from AeneasVerif/son/tuples
Do not use tuple projectors in the Lean backend
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 29 |
1 files changed, 22 insertions, 7 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index a5ba31bc..f45d7f23 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -446,27 +446,42 @@ let read_then_incr (x : u32) : result (u32 & u32) = Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *) type tuple_t (t1 t2 : Type0) = t1 * t2 -(** [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *) -let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = +(** [no_nested_borrows::read_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 *) +let read_tuple (x : (u32 & u32)) : result u32 = + let (i, _) = x in Ok i + +(** [no_nested_borrows::update_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 *) +let update_tuple (x : (u32 & u32)) : result (u32 & u32) = + let (_, i) = x in Ok (1, i) + +(** [no_nested_borrows::read_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 *) +let read_tuple_struct (x : tuple_t u32 u32) : result u32 = + let (i, _) = x in Ok i + +(** [no_nested_borrows::update_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 *) +let update_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = let (_, i) = x in Ok (1, i) (** [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *) + Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 *) let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) = Ok (x, y) (** [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 *) type idType_t (t : Type0) = t (** [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 *) let use_id_type (t : Type0) (x : idType_t t) : result t = Ok x (** [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *) + Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 *) let create_id_type (t : Type0) (x : t) : result (idType_t t) = Ok x |