summaryrefslogtreecommitdiff
path: root/tests/fstar/demo
diff options
context:
space:
mode:
authorSon HO2024-04-04 14:31:03 +0200
committerGitHub2024-04-04 14:31:03 +0200
commitb4f5719a10427dfc168f1210b05397599e761f9a (patch)
tree55906070f19df2a3185250df2aef36f47669842a /tests/fstar/demo
parent88cb18c614819f4abba1e0dfdb80c455d334d595 (diff)
parent0c3be2a82205d2737546c7ce8b15b6ad07f34095 (diff)
Merge pull request #111 from AeneasVerif/son/names
Improve the names used for the variables in the generated code
Diffstat (limited to 'tests/fstar/demo')
-rw-r--r--tests/fstar/demo/Demo.fst26
1 files changed, 12 insertions, 14 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d93bc847..9c59ab9b 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -10,8 +10,8 @@ open Primitives
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 *)
@@ -66,15 +66,14 @@ let rec list_nth_mut
| CList_CCons x tl ->
if i = 0
then
- let back_'a = fun ret -> Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in
- Return (x1, back_'a)
+ Return (x1, back)
| CList_CNil -> Fail Failure
end
@@ -92,14 +91,13 @@ let rec list_nth_mut1_loop
| CList_CCons x tl ->
if i = 0
then
- let back_'a = fun ret -> Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
- let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in
- let back_'a1 =
- fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in
- Return (x1, back_'a1)
+ let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
+ let back1 =
+ fun ret -> let* tl1 = back ret in Return (CList_CCons x tl1) in
+ Return (x1, back1)
| CList_CNil -> Fail Failure
end
@@ -135,10 +133,10 @@ let rec list_tail
begin match l with
| CList_CCons x tl ->
let* (c, list_tail_back) = list_tail t n1 tl in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1)
in
- Return (c, back_'a)
+ Return (c, back)
| CList_CNil -> Return (CList_CNil, Return)
end