diff options
| author | Son HO | 2023-08-09 09:58:04 +0200 |
|---|---|---|
| committer | GitHub | 2023-08-09 09:58:04 +0200 |
| commit | 3d377976afe382a32f6ce718b473db5f016b1e47 (patch) | |
| tree | 3f5b7147d1c4edc2b5c9ac002e1a203cfb396427 /tests/fstar/misc | |
| parent | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (diff) | |
| parent | 967d08107de73f7f151dc8b4fb1f1cc61f109051 (diff) | |
Merge pull request #33 from AeneasVerif/son_refactor
Update the code following Charon's refactor
Diffstat (limited to '')
| -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 |