summaryrefslogtreecommitdiff
path: root/tests/fstar/demo
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-31 13:09:37 +0200
committerAymeric Fromherz2024-05-31 13:09:37 +0200
commit092dae81f5f90281b634e229102d2dff7f5c3fd7 (patch)
treea12b32fb8c41844de6644fa0c36b658811598ec3 /tests/fstar/demo
parent1ee3d0f7d4f3c83351d5989c7979be3642069e63 (diff)
Regenerate test output
Diffstat (limited to 'tests/fstar/demo')
-rw-r--r--tests/fstar/demo/Demo.fst24
1 files changed, 23 insertions, 1 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index c78dab8e..41fd9804 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -76,13 +76,35 @@ let rec list_nth_mut
| CList_CNil -> Fail Failure
end
+(** [demo::list_nth_mut1]: loop 0:
+ Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
+let rec list_nth_mut1_loop
+ (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
+ result (t & (t -> result (cList_t t)))
+ =
+ if is_zero n
+ then Fail OutOfFuel
+ else
+ let n1 = decrease n in
+ begin match l with
+ | CList_CCons x tl ->
+ if i = 0
+ then let back = fun ret -> Ok (CList_CCons ret tl) in Ok (x, back)
+ else
+ let* i1 = u32_sub i 1 in
+ let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
+ let back1 = fun ret -> let* tl1 = back ret in Ok (CList_CCons x tl1) in
+ Ok (x1, back1)
+ | CList_CNil -> Fail Failure
+ end
+
(** [demo::list_nth_mut1]:
Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
let list_nth_mut1
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
=
- admit
+ list_nth_mut1_loop t n l i
(** [demo::i32_id]:
Source: 'tests/src/demo.rs', lines 80:0-80:28 *)