summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/PoloniusList.fst
diff options
context:
space:
mode:
authorSon Ho2024-04-04 16:20:20 +0200
committerSon Ho2024-04-04 16:20:20 +0200
commitb455f94c841b2423898f39bc9b6a4c35a3db56e3 (patch)
tree2311e681c45d9c7a27d7f728435837b3b6b41971 /tests/fstar/misc/PoloniusList.fst
parent57b71cb1bfde1832097163c7169aaf97cf8c7583 (diff)
Regenerate the test files
Diffstat (limited to 'tests/fstar/misc/PoloniusList.fst')
-rw-r--r--tests/fstar/misc/PoloniusList.fst10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 4203247e..c0bc592e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -20,13 +20,13 @@ let rec get_list_at_x
begin match ls with
| List_Cons hd tl ->
if hd = x
- then Return (List_Cons hd tl, Return)
+ then Ok (List_Cons hd tl, Ok)
else
let* (l, get_list_at_x_back) = get_list_at_x tl x in
let back =
- fun ret ->
- let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
- Return (l, back)
- | List_Nil -> Return (List_Nil, Return)
+ fun ret -> let* tl1 = get_list_at_x_back ret in Ok (List_Cons hd tl1)
+ in
+ Ok (l, back)
+ | List_Nil -> Ok (List_Nil, Ok)
end