summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/misc/NoNestedBorrows.fst20
1 files changed, 20 insertions, 0 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index fa7ad990..48186932 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -341,6 +341,26 @@ let rec list_nth_mut_back
| ListNil -> Fail
end
+(** [no_nested_borrows::list_rev_aux] *)
+let rec list_rev_aux_fwd
+ (t : Type0) (lo : list_t t) (li : list_t t) : result (list_t t) =
+ begin match li with
+ | ListCons hd tl ->
+ begin match list_rev_aux_fwd t (ListCons hd lo) tl with
+ | Fail -> Fail
+ | Return l -> Return l
+ end
+ | ListNil -> Return lo
+ end
+
+(** [no_nested_borrows::list_rev] *)
+let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
+ let l0 = mem_replace_fwd (list_t t) l ListNil in
+ begin match list_rev_aux_fwd t ListNil l0 with
+ | Fail -> Fail
+ | Return l1 -> Return l1
+ end
+
(** [no_nested_borrows::test_list_functions] *)
let test_list_functions_fwd : result unit =
let l = ListNil in