diff options
author | Son HO | 2024-03-20 06:48:08 +0100 |
---|---|---|
committer | GitHub | 2024-03-20 06:48:08 +0100 |
commit | 0d52c3fe35d0b24de729bdfb917ad6c7104d0c6e (patch) | |
tree | 7748d3c19a0993edc710690491a2dc6ea3a2b58f /tests/coq/misc/NoNestedBorrows.v | |
parent | 8111c970fcae9d609961eba2ad6716e8c9fc1046 (diff) | |
parent | 34850eed3c66f7f2c432294e4c589be53ad5d37b (diff) |
Merge pull request #93 from AeneasVerif/son/examples
Add some examples and improve the shape of the generated code
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 73c4ee58..76dc4cf6 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -475,9 +475,7 @@ Definition id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1) - in - Return ((x, y), back_'a) + Return ((x, y), Return) . (** [no_nested_borrows::id_mut_pair2]: @@ -486,10 +484,7 @@ Definition id_mut_pair2 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let (t, t1) := p in - let back_'a := - fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in - Return ((t, t1), back_'a) + let (t, t1) := p in Return ((t, t1), Return) . (** [no_nested_borrows::id_mut_pair3]: |