diff options
author | Son Ho | 2023-08-08 17:50:16 +0200 |
---|---|---|
committer | Son Ho | 2023-08-08 17:50:16 +0200 |
commit | 77f309cec8e2f119272640083bc3476e4121952c (patch) | |
tree | 79451f2f2b2d5e26ab0ad067b0bfe3c598f58a29 /tests/fstar/misc | |
parent | 6cdbb77f2be6f349729e2fd075ca3c51e9365b4f (diff) |
Regenerate the test files
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 12 |
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 |