summaryrefslogtreecommitdiff
path: root/tests/fstar-split/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar-split/betree')
-rw-r--r--tests/fstar-split/betree/BetreeMain.Funs.fst17
1 files changed, 6 insertions, 11 deletions
diff --git a/tests/fstar-split/betree/BetreeMain.Funs.fst b/tests/fstar-split/betree/BetreeMain.Funs.fst
index 6890488a..33133236 100644
--- a/tests/fstar-split/betree/BetreeMain.Funs.fst
+++ b/tests/fstar-split/betree/BetreeMain.Funs.fst
@@ -113,8 +113,7 @@ let rec betree_List_split_at
let* i = u64_sub n 1 in
let* p = betree_List_split_at t tl i in
let (ls0, ls1) = p in
- let l = ls0 in
- Return (Betree_List_Cons hd l, ls1)
+ Return (Betree_List_Cons hd ls0, ls1)
| Betree_List_Nil -> Fail Failure
end
@@ -124,8 +123,7 @@ let rec betree_List_split_at
let betree_List_push_front
(t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in
- let l = tl in
- Return (Betree_List_Cons x l)
+ Return (Betree_List_Cons x tl)
(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
Source: 'src/betree.rs', lines 306:4-306:32 *)
@@ -178,8 +176,7 @@ let rec betree_ListTupleU64T_partition_at_pivot
else
let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
let (ls0, ls1) = p in
- let l = ls0 in
- Return (Betree_List_Cons (i, x) l, ls1)
+ Return (Betree_List_Cons (i, x) ls0, ls1)
| Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
end
@@ -871,13 +868,12 @@ let betree_Node_apply
(new_msg : betree_Message_t) (st : state) :
result (state & unit)
=
- let l = Betree_List_Nil in
let* (st1, _) =
betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
- new_msg) l) st in
+ new_msg) Betree_List_Nil) st in
let* _ =
betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
- (key, new_msg) l) st in
+ (key, new_msg) Betree_List_Nil) st in
Return (st1, ())
(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
@@ -888,9 +884,8 @@ let betree_Node_apply_back
(new_msg : betree_Message_t) (st : state) :
result (betree_Node_t & betree_NodeIdCounter_t)
=
- let l = Betree_List_Nil in
betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
- (key, new_msg) l) st
+ (key, new_msg) Betree_List_Nil) st
(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
Source: 'src/betree.rs', lines 849:4-849:60 *)