Merge pull request #93 from AeneasVerif/son/examples

Add some examples and improve the shape of the generated code

10 files changed, 199 insertions, 216 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d637ee13..207f31b9 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -28,31 +28,26 @@ def array_to_mut_slice_
   (T : Type) (s : Array T 32#usize) :
   Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
   :=
-  do
-  let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s
-  Result.ret (s1, to_slice_mut_back)
+  Array.to_slice_mut T 32#usize s
 
 /- [arrays::array_len]:
    Source: 'src/arrays.rs', lines 25:0-25:40 -/
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_array_len]:
    Source: 'src/arrays.rs', lines 29:0-29:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
    Source: 'src/arrays.rs', lines 33:0-33:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
-  let i := Slice.len T s
-  Result.ret i
+  Result.ret (Slice.len T s)
 
 /- [arrays::index_array_shared]:
    Source: 'src/arrays.rs', lines 37:0-37:57 -/
@@ -76,9 +71,7 @@ def index_mut_array
   (T : Type) (s : Array T 32#usize) (i : Usize) :
   Result (T × (T → Result (Array T 32#usize)))
   :=
-  do
-  let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i
-  Result.ret (t, index_mut_back)
+  Array.index_mut_usize T 32#usize s i
 
 /- [arrays::index_slice]:
    Source: 'src/arrays.rs', lines 56:0-56:46 -/
@@ -91,9 +84,7 @@ def index_mut_slice
   (T : Type) (s : Slice T) (i : Usize) :
   Result (T × (T → Result (Slice T)))
   :=
-  do
-  let (t, index_mut_back) ← Slice.index_mut_usize T s i
-  Result.ret (t, index_mut_back)
+  Slice.index_mut_usize T s i
 
 /- [arrays::slice_subslice_shared_]:
    Source: 'src/arrays.rs', lines 64:0-64:70 -/
@@ -127,9 +118,7 @@ def array_to_slice_mut_
   (x : Array U32 32#usize) :
   Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
   :=
-  do
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x
-  Result.ret (s, to_slice_mut_back)
+  Array.to_slice_mut U32 32#usize x
 
 /- [arrays::array_subslice_shared_]:
    Source: 'src/arrays.rs', lines 80:0-80:74 -/
@@ -313,8 +302,8 @@ def update_all : Result Unit :=
   do
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a
+  let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
   let s1 ← update_mut_slice s
   let _ ← to_slice_mut_back s1
   Result.ret ()
@@ -354,9 +343,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit :=
 /- [arrays::non_copyable_array]:
    Source: 'src/arrays.rs', lines 229:0-229:27 -/
 def non_copyable_array : Result Unit :=
-  do
-  let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
-  Result.ret ()
+  take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
    Source: 'src/arrays.rs', lines 242:0-250:1 -/
@@ -496,11 +483,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
    Source: 'src/arrays.rs', lines 312:0-318:1 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
-  then
-    do
-    let i1 ← i + 1#usize
-    let _ ← iter_mut_slice_loop len i1
-    Result.ret ()
+  then do
+       let i1 ← i + 1#usize
+       iter_mut_slice_loop len i1
   else Result.ret ()
 
 /- [arrays::iter_mut_slice]:
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index d6449b37..ca9b48da 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -21,9 +21,7 @@ def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_internal_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_internal_node id content st
 
 /- [betree_main::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
@@ -37,9 +35,7 @@ def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_leaf_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_leaf_node id content st
 
 /- [betree_main::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
@@ -172,13 +168,13 @@ def betree.Leaf.split
   let (content0, content1) := p
   let p1 ← betree.List.hd (U64 × U64) content1
   let (pivot, _) := p1
-  let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
-  let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic
+  let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1
   let (st1, _) ← betree.store_leaf_node id0 content0 st
   let (st2, _) ← betree.store_leaf_node id1 content1 st1
   let n := betree.Node.Leaf { id := id0, size := params.split_size }
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
-  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1))
+  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
@@ -231,7 +227,7 @@ divergent def betree.Node.apply_upserts
   if b
   then
     do
-    let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs
+    let (msg, msgs1) ← betree.List.pop_front (U64 × betree.Message) msgs
     let (_, m) := msg
     match m with
     | betree.Message.Insert _ => Result.fail .panic
@@ -239,14 +235,14 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts l (some v) key st
+      betree.Node.apply_upserts msgs1 (some v) key st
   else
     do
     let (st1, v) ← core.option.Option.unwrap U64 prev st
-    let l ←
+    let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ret (st1, (v, l))
+    Result.ret (st1, (v, msgs1))
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
@@ -284,12 +280,12 @@ divergent def betree.Node.lookup
       if k != key
       then
         do
-        let (st2, (o, i2)) ←
+        let (st2, (o, node1)) ←
           betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
             st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
-        Result.ret (st2, (o, betree.Node.Internal i2))
+        Result.ret (st2, (o, betree.Node.Internal node1))
       else
         match msg with
         | betree.Message.Insert v =>
@@ -308,24 +304,24 @@ divergent def betree.Node.lookup
             n n1)))
         | betree.Message.Upsert ufs =>
           do
-          let (st2, (v, i2)) ←
+          let (st2, (v, node1)) ←
             betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
               key st1
-          let (st3, (v1, l1)) ←
+          let (st3, (v1, pending1)) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
               betree.Message.Upsert ufs) l) v key st2
-          let ⟨ i3, i4, n2, n3 ⟩ := i2
-          let msgs1 ← lookup_first_message_for_key_back l1
-          let (st4, _) ← betree.store_internal_node i3 msgs1 st3
+          let ⟨ i2, i3, n2, n3 ⟩ := node1
+          let msgs1 ← lookup_first_message_for_key_back pending1
+          let (st4, _) ← betree.store_internal_node i2 msgs1 st3
           Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
-            i3 i4 n2 n3)))
+            i2 i3 n2 n3)))
     | betree.List.Nil =>
       do
-      let (st2, (o, i2)) ←
+      let (st2, (o, node1)) ←
         betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
           st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
-      Result.ret (st2, (o, betree.Node.Internal i2))
+      Result.ret (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
     do
     let (st1, bindings) ← betree.load_leaf_node node.id st
@@ -346,10 +342,10 @@ divergent def betree.Node.filter_messages_for_key
     if k = key
     then
       do
-      let (_, l1) ←
+      let (_, msgs1) ←
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
-      betree.Node.filter_messages_for_key key l1
+      betree.Node.filter_messages_for_key key msgs1
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
@@ -393,18 +389,18 @@ def betree.Node.apply_to_internal
     match new_msg with
     | betree.Message.Insert i =>
       do
-      let l ← betree.Node.filter_messages_for_key key msgs1
-      let l1 ←
-        betree.List.push_front (U64 × betree.Message) l (key,
+      let msgs2 ← betree.Node.filter_messages_for_key key msgs1
+      let msgs3 ←
+        betree.List.push_front (U64 × betree.Message) msgs2 (key,
           betree.Message.Insert i)
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | betree.Message.Delete =>
       do
-      let l ← betree.Node.filter_messages_for_key key msgs1
-      let l1 ←
-        betree.List.push_front (U64 × betree.Message) l (key,
+      let msgs2 ← betree.Node.filter_messages_for_key key msgs1
+      let msgs3 ←
+        betree.List.push_front (U64 × betree.Message) msgs2 (key,
           betree.Message.Delete)
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | betree.Message.Upsert s =>
       do
       let p ← betree.List.hd (U64 × betree.Message) msgs1
@@ -413,33 +409,33 @@ def betree.Node.apply_to_internal
       | betree.Message.Insert prev =>
         do
         let v ← betree.upsert_update (some prev) s
-        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
-        let l1 ←
-          betree.List.push_front (U64 × betree.Message) l (key,
+        let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let msgs3 ←
+          betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Insert v)
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | betree.Message.Delete =>
         do
-        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1
         let v ← betree.upsert_update none s
-        let l1 ←
-          betree.List.push_front (U64 × betree.Message) l (key,
+        let msgs3 ←
+          betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Insert v)
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | betree.Message.Upsert _ =>
         do
         let (msgs2, lookup_first_message_after_key_back) ←
           betree.Node.lookup_first_message_after_key key msgs1
-        let l ←
+        let msgs3 ←
           betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Upsert s)
-        let msgs3 ← lookup_first_message_after_key_back l
-        lookup_first_message_for_key_back msgs3
+        let msgs4 ← lookup_first_message_after_key_back msgs3
+        lookup_first_message_for_key_back msgs4
   else
     do
-    let l ←
+    let msgs2 ←
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
-    lookup_first_message_for_key_back l
+    lookup_first_message_for_key_back msgs2
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 502:4-505:5 -/
@@ -452,8 +448,8 @@ divergent def betree.Node.apply_messages_to_internal
   | betree.List.Cons new_msg new_msgs_tl =>
     do
     let (i, m) := new_msg
-    let l ← betree.Node.apply_to_internal msgs i m
-    betree.Node.apply_messages_to_internal l new_msgs_tl
+    let msgs1 ← betree.Node.apply_to_internal msgs i m
+    betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
@@ -494,31 +490,31 @@ def betree.Node.apply_to_leaf
   if b
   then
     do
-    let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1
+    let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1
     match new_msg with
     | betree.Message.Insert v =>
       do
-      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
-      lookup_mut_in_bindings_back l1
-    | betree.Message.Delete => lookup_mut_in_bindings_back l
+      let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v)
+      lookup_mut_in_bindings_back bindings3
+    | betree.Message.Delete => lookup_mut_in_bindings_back bindings2
     | betree.Message.Upsert s =>
       do
       let (_, i) := hd
       let v ← betree.upsert_update (some i) s
-      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
-      lookup_mut_in_bindings_back l1
+      let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v)
+      lookup_mut_in_bindings_back bindings3
   else
     match new_msg with
     | betree.Message.Insert v =>
       do
-      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
-      lookup_mut_in_bindings_back l
+      let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back bindings2
     | betree.Message.Delete => lookup_mut_in_bindings_back bindings1
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update none s
-      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
-      lookup_mut_in_bindings_back l
+      let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back bindings2
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 444:4-447:5 -/
@@ -531,8 +527,8 @@ divergent def betree.Node.apply_messages_to_leaf
   | betree.List.Cons new_msg new_msgs_tl =>
     do
     let (i, m) := new_msg
-    let l ← betree.Node.apply_to_leaf bindings i m
-    betree.Node.apply_messages_to_leaf l new_msgs_tl
+    let bindings1 ← betree.Node.apply_to_leaf bindings i m
+    betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
@@ -587,40 +583,40 @@ divergent def betree.Node.apply_messages
     do
     let ⟨ i, i1, n, n1 ⟩ := node
     let (st1, content) ← betree.load_internal_node i st
-    let l ← betree.Node.apply_messages_to_internal content msgs
-    let num_msgs ← betree.List.len (U64 × betree.Message) l
+    let content1 ← betree.Node.apply_messages_to_internal content msgs
+    let num_msgs ← betree.List.len (U64 × betree.Message) content1
     if num_msgs >= params.min_flush_size
     then
       do
-      let (st2, (content1, p)) ←
+      let (st2, (content2, p)) ←
         betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
-          l st1
+          content1 st1
       let (node1, node_id_cnt1) := p
       let ⟨ i2, i3, n2, n3 ⟩ := node1
-      let (st3, _) ← betree.store_internal_node i2 content1 st2
+      let (st3, _) ← betree.store_internal_node i2 content2 st2
       Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
         node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_internal_node i l st1
+      let (st2, _) ← betree.store_internal_node i content1 st1
       Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
         node_id_cnt))
   | betree.Node.Leaf node =>
     do
     let (st1, content) ← betree.load_leaf_node node.id st
-    let l ← betree.Node.apply_messages_to_leaf content msgs
-    let len ← betree.List.len (U64 × U64) l
+    let content1 ← betree.Node.apply_messages_to_leaf content msgs
+    let len ← betree.List.len (U64 × U64) content1
     let i ← 2#u64 * params.split_size
     if len >= i
     then
       do
-      let (st2, (new_node, nic)) ←
-        betree.Leaf.split node l params node_id_cnt st1
+      let (st2, (new_node, node_id_cnt1)) ←
+        betree.Leaf.split node content1 params node_id_cnt st1
       let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
-      Result.ret (st3, (betree.Node.Internal new_node, nic))
+      Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_leaf_node node.id l st1
+      let (st2, _) ← betree.store_leaf_node node.id content1 st1
       Result.ret (st2, (betree.Node.Leaf { node with size := len },
         node_id_cnt))
 
@@ -649,12 +645,12 @@ def betree.BeTree.new
   :=
   do
   let node_id_cnt ← betree.NodeIdCounter.new
-  let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
   let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
   Result.ret (st1,
     {
       params := { min_flush_size := min_flush_size, split_size := split_size },
-      node_id_cnt := nic,
+      node_id_cnt := node_id_cnt1,
       root := (betree.Node.Leaf { id := id, size := 0#u64 })
     })
 
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 854b4853..4acc69c8 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
+/- [demo::use_incr]:
+   Source: 'src/demo.rs', lines 25:0-25:17 -/
+def use_incr : Result Unit :=
+  do
+  let x ← incr 0#u32
+  let x1 ← incr x
+  let _ ← incr x1
+  Result.ret ()
+
 /- [demo::CList]
-   Source: 'src/demo.rs', lines 27:0-27:17 -/
+   Source: 'src/demo.rs', lines 34:0-34:17 -/
 inductive CList (T : Type) :=
 | CCons : T → CList T → CList T
 | CNil : CList T
 
 /- [demo::list_nth]:
-   Source: 'src/demo.rs', lines 32:0-32:56 -/
+   Source: 'src/demo.rs', lines 39:0-39:56 -/
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
@@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut]:
-   Source: 'src/demo.rs', lines 47:0-47:68 -/
+   Source: 'src/demo.rs', lines 54:0-54:68 -/
 divergent def list_nth_mut
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -79,7 +88,7 @@ divergent def list_nth_mut
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
-   Source: 'src/demo.rs', lines 62:0-71:1 -/
+   Source: 'src/demo.rs', lines 69:0-78:1 -/
 divergent def list_nth_mut1_loop
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -102,17 +111,15 @@ divergent def list_nth_mut1_loop
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
-   Source: 'src/demo.rs', lines 62:0-62:77 -/
+   Source: 'src/demo.rs', lines 69:0-69:77 -/
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
   :=
-  do
-  let (t, back_'a) ← list_nth_mut1_loop T l i
-  Result.ret (t, back_'a)
+  list_nth_mut1_loop T l i
 
 /- [demo::i32_id]:
-   Source: 'src/demo.rs', lines 73:0-73:28 -/
+   Source: 'src/demo.rs', lines 80:0-80:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
   then Result.ret 0#i32
@@ -121,26 +128,44 @@ divergent def i32_id (i : I32) : Result I32 :=
        let i2 ← i32_id i1
        i2 + 1#i32
 
+/- [demo::list_tail]:
+   Source: 'src/demo.rs', lines 88:0-88:64 -/
+divergent def list_tail
+  (T : Type) (l : CList T) :
+  Result ((CList T) × (CList T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons t tl =>
+    do
+    let (c, list_tail_back) ← list_tail T tl
+    let back_'a :=
+      fun ret =>
+        do
+        let tl1 ← list_tail_back ret
+        Result.ret (CList.CCons t tl1)
+    Result.ret (c, back_'a)
+  | CList.CNil => Result.ret (CList.CNil, Result.ret)
+
 /- Trait declaration: [demo::Counter]
-   Source: 'src/demo.rs', lines 83:0-83:17 -/
+   Source: 'src/demo.rs', lines 97:0-97:17 -/
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
 /- [demo::{(demo::Counter for usize)}::incr]:
-   Source: 'src/demo.rs', lines 88:4-88:31 -/
+   Source: 'src/demo.rs', lines 102:4-102:31 -/
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ret (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
-   Source: 'src/demo.rs', lines 87:0-87:22 -/
+   Source: 'src/demo.rs', lines 101:0-101:22 -/
 def CounterUsize : Counter Usize := {
   incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
-   Source: 'src/demo.rs', lines 95:0-95:59 -/
+   Source: 'src/demo.rs', lines 109:0-109:59 -/
 def use_counter
   (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
   CounterInst.incr cnt
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index cdec7332..e514ac3e 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
 termination_by x.val.toNat
 decreasing_by scalar_decr_tac
 
+theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
+  ∃ back, list_tail T l = ret (CList.CNil, back) ∧
+  ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+  rw [list_tail]
+  match l with
+  | CNil =>
+    simp_all
+  | CCons hd tl =>
+    simp_all
+    progress as ⟨ back ⟩
+    simp
+    -- Proving the backward function
+    intro tl'
+    progress
+    simp_all
+
 end demo
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index db15aacc..8b645037 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -38,9 +38,9 @@ def custom_swap
   Result (State × (T × (T → State → Result (State × (T × T)))))
   :=
   do
-  let (st1, (t, t1)) ← core.mem.swap T x y st
-  let back_'a := fun ret st2 => Result.ret (st2, (ret, t1))
-  Result.ret (st1, (t, back_'a))
+  let (st1, (x1, y1)) ← core.mem.swap T x y st
+  let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
+  Result.ret (st1, (x1, back_'a))
 
 /- [external::test_custom_swap]:
    Source: 'src/external.rs', lines 29:0-29:59 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f0706725..1c95f7c9 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -20,9 +20,9 @@ divergent def HashMap.allocate_slots_loop
   if n > 0#usize
   then
     do
-    let v ← alloc.vec.Vec.push (List T) slots List.Nil
+    let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
     let n1 ← n - 1#usize
-    HashMap.allocate_slots_loop T v n1
+    HashMap.allocate_slots_loop T slots1 n1
   else Result.ret slots
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
@@ -142,8 +142,8 @@ divergent def HashMap.move_elements_from_list_loop
   match ls with
   | List.Cons k v tl =>
     do
-    let hm ← HashMap.insert_no_resize T ntable k v
-    HashMap.move_elements_from_list_loop T hm tl
+    let ntable1 ← HashMap.insert_no_resize T ntable k v
+    HashMap.move_elements_from_list_loop T ntable1 tl
   | List.Nil => Result.ret ntable
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
@@ -167,12 +167,10 @@ divergent def HashMap.move_elements_loop
       alloc.vec.Vec.index_mut (List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
     let (ls, l1) := core.mem.replace (List T) l List.Nil
-    let hm ← HashMap.move_elements_from_list T ntable ls
+    let ntable1 ← HashMap.move_elements_from_list T ntable ls
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
-    let back_'a ← HashMap.move_elements_loop T hm slots1 i2
-    let (hm1, v) := back_'a
-    Result.ret (hm1, v)
+    HashMap.move_elements_loop T ntable1 slots1 i2
   else Result.ret (ntable, slots)
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
@@ -182,10 +180,7 @@ def HashMap.move_elements
   :
   Result ((HashMap T) × (alloc.vec.Vec (List T)))
   :=
-  do
-  let back_'a ← HashMap.move_elements_loop T ntable slots i
-  let (hm, v) := back_'a
-  Result.ret (hm, v)
+  HashMap.move_elements_loop T ntable slots i
 
 /- [hashmap::{hashmap::HashMap<T>}::try_resize]:
    Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -218,11 +213,11 @@ def HashMap.insert
   Result (HashMap T)
   :=
   do
-  let hm ← HashMap.insert_no_resize T self key value
-  let i ← HashMap.len T hm
-  if i > hm.max_load
-  then HashMap.try_resize T hm
-  else Result.ret hm
+  let self1 ← HashMap.insert_no_resize T self key value
+  let i ← HashMap.len T self1
+  if i > self1.max_load
+  then HashMap.try_resize T self1
+  else Result.ret self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -311,9 +306,7 @@ def HashMap.get_mut_in_list
   (T : Type) (ls : List T) (key : Usize) :
   Result (T × (T → Result (List T)))
   :=
-  do
-  let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 31441b4a..6a6934b8 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -21,9 +21,9 @@ divergent def hashmap.HashMap.allocate_slots_loop
   if n > 0#usize
   then
     do
-    let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
+    let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
     let n1 ← n - 1#usize
-    hashmap.HashMap.allocate_slots_loop T v n1
+    hashmap.HashMap.allocate_slots_loop T slots1 n1
   else Result.ret slots
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
@@ -150,8 +150,8 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
   match ls with
   | hashmap.List.Cons k v tl =>
     do
-    let hm ← hashmap.HashMap.insert_no_resize T ntable k v
-    hashmap.HashMap.move_elements_from_list_loop T hm tl
+    let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
+    hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
   | hashmap.List.Nil => Result.ret ntable
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
@@ -177,12 +177,10 @@ divergent def hashmap.HashMap.move_elements_loop
       alloc.vec.Vec.index_mut (hashmap.List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i
     let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil
-    let hm ← hashmap.HashMap.move_elements_from_list T ntable ls
+    let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
-    let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2
-    let (hm1, v) := back_'a
-    Result.ret (hm1, v)
+    hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
   else Result.ret (ntable, slots)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
@@ -192,10 +190,7 @@ def hashmap.HashMap.move_elements
   (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
   Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
   :=
-  do
-  let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i
-  let (hm, v) := back_'a
-  Result.ret (hm, v)
+  hashmap.HashMap.move_elements_loop T ntable slots i
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
    Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -229,11 +224,11 @@ def hashmap.HashMap.insert
   Result (hashmap.HashMap T)
   :=
   do
-  let hm ← hashmap.HashMap.insert_no_resize T self key value
-  let i ← hashmap.HashMap.len T hm
-  if i > hm.max_load
-  then hashmap.HashMap.try_resize T hm
-  else Result.ret hm
+  let self1 ← hashmap.HashMap.insert_no_resize T self key value
+  let i ← hashmap.HashMap.len T self1
+  if i > self1.max_load
+  then hashmap.HashMap.try_resize T self1
+  else Result.ret self1
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -326,9 +321,7 @@ def hashmap.HashMap.get_mut_in_list
   (T : Type) (ls : hashmap.List T) (key : Usize) :
   Result (T × (T → Result (hashmap.List T)))
   :=
-  do
-  let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  hashmap.HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -460,8 +453,7 @@ def insert_on_disk
   do
   let (st1, hm) ← hashmap_utils.deserialize st
   let hm1 ← hashmap.HashMap.insert U64 hm key value
-  let (st2, _) ← hashmap_utils.serialize hm1 st1
-  Result.ret (st2, ())
+  hashmap_utils.serialize hm1 st1
 
 /- [hashmap_main::main]:
    Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 433ca8f0..0f3d77c2 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -23,14 +23,14 @@ def sum (max : U32) : Result U32 :=
 /- [loops::sum_with_mut_borrows]: loop 0:
    Source: 'src/loops.rs', lines 19:0-31:1 -/
 divergent def sum_with_mut_borrows_loop
-  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
-  if mi < max
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
   then
     do
-    let ms1 ← ms + mi
-    let mi1 ← mi + 1#u32
-    sum_with_mut_borrows_loop max mi1 ms1
-  else ms * 2#u32
+    let ms ← s + i
+    let mi ← i + 1#u32
+    sum_with_mut_borrows_loop max mi ms
+  else s * 2#u32
 
 /- [loops::sum_with_mut_borrows]:
    Source: 'src/loops.rs', lines 19:0-19:44 -/
@@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop
    Source: 'src/loops.rs', lines 88:0-88:71 -/
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
-  do
-  let (t, back) ← list_nth_mut_loop_loop T ls i
-  Result.ret (t, back)
+  list_nth_mut_loop_loop T ls i
 
 /- [loops::list_nth_shared_loop]: loop 0:
    Source: 'src/loops.rs', lines 101:0-111:1 -/
@@ -189,13 +187,13 @@ def get_elem_mut
   Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
   :=
   do
-  let (l, index_mut_back) ←
+  let (ls, index_mut_back) ←
     alloc.vec.Vec.index_mut (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  let (i, back) ← get_elem_mut_loop x l
+  let (i, back) ← get_elem_mut_loop x ls
   let back1 := fun ret => do
-                          let l1 ← back ret
-                          index_mut_back l1
+                          let l ← back ret
+                          index_mut_back l
   Result.ret (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
@@ -213,10 +211,10 @@ divergent def get_elem_shared_loop
 def get_elem_shared
   (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-  let l ←
+  let ls ←
     alloc.vec.Vec.index (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  get_elem_shared_loop x l
+  get_elem_shared_loop x ls
 
 /- [loops::id_mut]:
    Source: 'src/loops.rs', lines 145:0-145:50 -/
@@ -322,9 +320,7 @@ def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 208:0-229:1 -/
@@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 251:0-266:1 -/
@@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 288:0-303:1 -/
@@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 307:0-322:1 -/
@@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'b)
+  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 326:0-341:1 -/
@@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'src/loops.rs', lines 345:0-349:1 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_mut_borrow]:
@@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 353:0-358:1 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← incr_ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       incr_ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::incr_ignore_input_mut_borrow]:
@@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 362:0-366:1 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_shared_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_shared_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_shared_borrow]:
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 2112e282..5f9ec0f2 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -487,9 +487,7 @@ def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
-  let back_'a := fun ret => let (t, t1) := ret
-                            Result.ret (t, t1)
-  Result.ret ((x, y), back_'a)
+  Result.ret ((x, y), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair2]:
    Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -498,9 +496,7 @@ def id_mut_pair2
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
   let (t, t1) := p
-  let back_'a := fun ret => let (t2, t3) := ret
-                            Result.ret (t2, t3)
-  Result.ret ((t, t1), back_'a)
+  Result.ret ((t, t1), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair3]:
    Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 4930a05c..924ff36c 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -14,8 +14,8 @@ def ref_incr (x : I32) : Result I32 :=
    Source: 'src/paper.rs', lines 8:0-8:18 -/
 def test_incr : Result Unit :=
   do
-  let i ← ref_incr 0#i32
-  if ¬ (i = 1#i32)
+  let x ← ref_incr 0#i32
+  if ¬ (x = 1#i32)
   then Result.fail .panic
   else Result.ret ()