summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
authorSon Ho2023-08-08 17:50:16 +0200
committerSon Ho2023-08-08 17:50:16 +0200
commit77f309cec8e2f119272640083bc3476e4121952c (patch)
tree79451f2f2b2d5e26ab0ad067b0bfe3c598f58a29 /tests/fstar/misc
parent6cdbb77f2be6f349729e2fd075ca3c51e9365b4f (diff)
Regenerate the test files
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst12
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index d790bfa9..2cdd6e21 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -202,16 +202,16 @@ let _ = assert_norm (choose_test_fwd = Return ())
let test_char_fwd : result char =
Return 'a'
-(** [no_nested_borrows::NodeElem] *)
-type node_elem_t (t : Type0) =
-| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
-| NodeElemNil : node_elem_t t
-
(** [no_nested_borrows::Tree] *)
-and tree_t (t : Type0) =
+type tree_t (t : Type0) =
| TreeLeaf : t -> tree_t t
| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
+(** [no_nested_borrows::NodeElem] *)
+and node_elem_t (t : Type0) =
+| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
+| NodeElemNil : node_elem_t t
+
(** [no_nested_borrows::list_length]: forward function *)
let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
begin match l with