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