Merge pull request #49 from AeneasVerif/son_merge_back

Allow the extraction of structures as tuples

1 files changed, 30 insertions, 1 deletions

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 0c7dff8e..8ee8ad9e 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -35,7 +35,7 @@ inductive Enum :=
 
 /- [no_nested_borrows::EmptyStruct]
    Source: 'src/no_nested_borrows.rs', lines 39:0-39:22 -/
-structure EmptyStruct where
+@[reducible] def EmptyStruct := Unit
 
 /- [no_nested_borrows::Sum]
    Source: 'src/no_nested_borrows.rs', lines 41:0-41:20 -/
@@ -643,4 +643,33 @@ def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
 def test_shared_borrow_enum2 : Result U32 :=
   Result.ret 0#u32
 
+/- [no_nested_borrows::Tuple]
+   Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 -/
+def Tuple (T1 T2 : Type) := T1 × T2
+
+/- [no_nested_borrows::use_tuple_struct]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ())
+   Source: 'src/no_nested_borrows.rs', lines 532:0-532:48 -/
+def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
+  Result.ret (1#u32, x.1)
+
+/- [no_nested_borrows::create_tuple_struct]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 -/
+def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
+  Result.ret (x, y)
+
+/- [no_nested_borrows::IdType]
+   Source: 'src/no_nested_borrows.rs', lines 541:0-541:20 -/
+@[reducible] def IdType (T : Type) := T
+
+/- [no_nested_borrows::use_id_type]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 -/
+def use_id_type (T : Type) (x : IdType T) : Result T :=
+  Result.ret x
+
+/- [no_nested_borrows::create_id_type]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 547:0-547:43 -/
+def create_id_type (T : Type) (x : T) : Result (IdType T) :=
+  Result.ret x
+
 end no_nested_borrows