From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 14:57:51 +0200
Subject: Reorganize the Lean tests

---
 tests/lean/Loops/Funs.lean  | 624 ++++++++++++++++++++++++++++++++++++++++++++
 tests/lean/Loops/Types.lean |  10 +
 2 files changed, 634 insertions(+)
 create mode 100644 tests/lean/Loops/Funs.lean
 create mode 100644 tests/lean/Loops/Types.lean

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
new file mode 100644
index 00000000..7d5f7595
--- /dev/null
+++ b/tests/lean/Loops/Funs.lean
@@ -0,0 +1,624 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [loops]: function definitions
+import Base
+import Loops.Types
+open Primitives
+
+/- [loops::sum] -/
+divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
+  then
+    do
+      let s0 ← s + i
+      let i0 ← i + (U32.ofInt 1 (by intlit))
+      sum_loop_fwd max i0 s0
+  else s * (U32.ofInt 2 (by intlit))
+
+/- [loops::sum] -/
+def sum_fwd (max : U32) : Result U32 :=
+  sum_loop_fwd max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
+
+/- [loops::sum_with_mut_borrows] -/
+divergent def sum_with_mut_borrows_loop_fwd
+  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
+  if mi < max
+  then
+    do
+      let ms0 ← ms + mi
+      let mi0 ← mi + (U32.ofInt 1 (by intlit))
+      sum_with_mut_borrows_loop_fwd max mi0 ms0
+  else ms * (U32.ofInt 2 (by intlit))
+
+/- [loops::sum_with_mut_borrows] -/
+def sum_with_mut_borrows_fwd (max : U32) : Result U32 :=
+  sum_with_mut_borrows_loop_fwd max (U32.ofInt 0 (by intlit))
+    (U32.ofInt 0 (by intlit))
+
+/- [loops::sum_with_shared_borrows] -/
+divergent def sum_with_shared_borrows_loop_fwd
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
+  then
+    do
+      let i0 ← i + (U32.ofInt 1 (by intlit))
+      let s0 ← s + i0
+      sum_with_shared_borrows_loop_fwd max i0 s0
+  else s * (U32.ofInt 2 (by intlit))
+
+/- [loops::sum_with_shared_borrows] -/
+def sum_with_shared_borrows_fwd (max : U32) : Result U32 :=
+  sum_with_shared_borrows_loop_fwd max (U32.ofInt 0 (by intlit))
+    (U32.ofInt 0 (by intlit))
+
+/- [loops::clear] -/
+divergent def clear_loop_fwd_back
+  (v : Vec U32) (i : Usize) : Result (Vec U32) :=
+  let i0 := vec_len U32 v
+  if i < i0
+  then
+    do
+      let i1 ← i + (Usize.ofInt 1 (by intlit))
+      let v0 ← vec_index_mut_back U32 v i (U32.ofInt 0 (by intlit))
+      clear_loop_fwd_back v0 i1
+  else Result.ret v
+
+/- [loops::clear] -/
+def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
+  clear_loop_fwd_back v (Usize.ofInt 0 (by intlit))
+
+/- [loops::list_mem] -/
+divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool :=
+  match h: ls with
+  | list_t.Cons y tl =>
+    if y = x
+    then Result.ret true
+    else list_mem_loop_fwd x tl
+  | list_t.Nil => Result.ret false
+
+/- [loops::list_mem] -/
+def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool :=
+  list_mem_loop_fwd x ls
+
+/- [loops::list_nth_mut_loop] -/
+divergent def list_nth_mut_loop_loop_fwd
+  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret x
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        list_nth_mut_loop_loop_fwd T tl i0
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop] -/
+def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  list_nth_mut_loop_loop_fwd T ls i
+
+/- [loops::list_nth_mut_loop] -/
+divergent def list_nth_mut_loop_loop_back
+  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret (list_t.Cons ret0 tl)
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop] -/
+def list_nth_mut_loop_back
+  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  list_nth_mut_loop_loop_back T ls i ret0
+
+/- [loops::list_nth_shared_loop] -/
+divergent def list_nth_shared_loop_loop_fwd
+  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret x
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        list_nth_shared_loop_loop_fwd T tl i0
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop] -/
+def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  list_nth_shared_loop_loop_fwd T ls i
+
+/- [loops::get_elem_mut] -/
+divergent def get_elem_mut_loop_fwd
+  (x : Usize) (ls : list_t Usize) : Result Usize :=
+  match h: ls with
+  | list_t.Cons y tl =>
+    if y = x
+    then Result.ret y
+    else get_elem_mut_loop_fwd x tl
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_mut] -/
+def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
+  do
+    let l ←
+      vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    get_elem_mut_loop_fwd x l
+
+/- [loops::get_elem_mut] -/
+divergent def get_elem_mut_loop_back
+  (x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) :=
+  match h: ls with
+  | list_t.Cons y tl =>
+    if y = x
+    then Result.ret (list_t.Cons ret0 tl)
+    else
+      do
+        let tl0 ← get_elem_mut_loop_back x tl ret0
+        Result.ret (list_t.Cons y tl0)
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_mut] -/
+def get_elem_mut_back
+  (slots : Vec (list_t Usize)) (x : Usize) (ret0 : Usize) :
+  Result (Vec (list_t Usize))
+  :=
+  do
+    let l ←
+      vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    let l0 ← get_elem_mut_loop_back x l ret0
+    vec_index_mut_back (list_t Usize) slots (Usize.ofInt 0 (by intlit)) l0
+
+/- [loops::get_elem_shared] -/
+divergent def get_elem_shared_loop_fwd
+  (x : Usize) (ls : list_t Usize) : Result Usize :=
+  match h: ls with
+  | list_t.Cons y tl =>
+    if y = x
+    then Result.ret y
+    else get_elem_shared_loop_fwd x tl
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::get_elem_shared] -/
+def get_elem_shared_fwd
+  (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
+  do
+    let l ← vec_index_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    get_elem_shared_loop_fwd x l
+
+/- [loops::id_mut] -/
+def id_mut_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
+  Result.ret ls
+
+/- [loops::id_mut] -/
+def id_mut_back
+  (T : Type) (ls : list_t T) (ret0 : list_t T) : Result (list_t T) :=
+  Result.ret ret0
+
+/- [loops::id_shared] -/
+def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
+  Result.ret ls
+
+/- [loops::list_nth_mut_loop_with_id] -/
+divergent def list_nth_mut_loop_with_id_loop_fwd
+  (T : Type) (i : U32) (ls : list_t T) : Result T :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret x
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        list_nth_mut_loop_with_id_loop_fwd T i0 tl
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_with_id] -/
+def list_nth_mut_loop_with_id_fwd
+  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  do
+    let ls0 ← id_mut_fwd T ls
+    list_nth_mut_loop_with_id_loop_fwd T i ls0
+
+/- [loops::list_nth_mut_loop_with_id] -/
+divergent def list_nth_mut_loop_with_id_loop_back
+  (T : Type) (i : U32) (ls : list_t T) (ret0 : T) : Result (list_t T) :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret (list_t.Cons ret0 tl)
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_with_id] -/
+def list_nth_mut_loop_with_id_back
+  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  do
+    let ls0 ← id_mut_fwd T ls
+    let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0
+    id_mut_back T ls l
+
+/- [loops::list_nth_shared_loop_with_id] -/
+divergent def list_nth_shared_loop_with_id_loop_fwd
+  (T : Type) (i : U32) (ls : list_t T) : Result T :=
+  match h: ls with
+  | list_t.Cons x tl =>
+    if i = (U32.ofInt 0 (by intlit))
+    then Result.ret x
+    else
+      do
+        let i0 ← i - (U32.ofInt 1 (by intlit))
+        list_nth_shared_loop_with_id_loop_fwd T i0 tl
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop_with_id] -/
+def list_nth_shared_loop_with_id_fwd
+  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  do
+    let ls0 ← id_shared_fwd T ls
+    list_nth_shared_loop_with_id_loop_fwd T i ls0
+
+/- [loops::list_nth_mut_loop_pair] -/
+divergent def list_nth_mut_loop_pair_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair] -/
+def list_nth_mut_loop_pair_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_mut_loop_pair_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair] -/
+divergent def list_nth_mut_loop_pair_loop_back'a
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair] -/
+def list_nth_mut_loop_pair_back'a
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
+
+/- [loops::list_nth_mut_loop_pair] -/
+divergent def list_nth_mut_loop_pair_loop_back'b
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair] -/
+def list_nth_mut_loop_pair_back'b
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_loop_pair] -/
+divergent def list_nth_shared_loop_pair_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop_pair] -/
+def list_nth_shared_loop_pair_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_shared_loop_pair_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair_merge] -/
+divergent def list_nth_mut_loop_pair_merge_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair_merge] -/
+def list_nth_mut_loop_pair_merge_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_loop_pair_merge] -/
+divergent def list_nth_mut_loop_pair_merge_loop_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
+  Result ((list_t T) × (list_t T))
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then
+        let (t, t0) := ret0
+        Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let (tl00, tl10) ←
+            list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x0 tl00, list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_loop_pair_merge] -/
+def list_nth_mut_loop_pair_merge_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
+  Result ((list_t T) × (list_t T))
+  :=
+  list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_loop_pair_merge] -/
+divergent def list_nth_shared_loop_pair_merge_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_loop_pair_merge] -/
+def list_nth_shared_loop_pair_merge_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair] -/
+divergent def list_nth_mut_shared_loop_pair_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair] -/
+def list_nth_mut_shared_loop_pair_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_mut_shared_loop_pair_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair] -/
+divergent def list_nth_mut_shared_loop_pair_loop_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl00 ←
+            list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair] -/
+def list_nth_mut_shared_loop_pair_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+def list_nth_mut_shared_loop_pair_merge_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_mut_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+divergent def list_nth_mut_shared_loop_pair_merge_loop_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl0)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl00 ←
+            list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+def list_nth_mut_shared_loop_pair_merge_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_mut_loop_pair] -/
+divergent def list_nth_shared_mut_loop_pair_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair] -/
+def list_nth_shared_mut_loop_pair_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_shared_mut_loop_pair_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_shared_mut_loop_pair] -/
+divergent def list_nth_shared_mut_loop_pair_loop_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl10 ←
+            list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair] -/
+def list_nth_shared_mut_loop_pair_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
+
+/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (x0, x1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+def list_nth_shared_mut_loop_pair_merge_fwd
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  list_nth_shared_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
+
+/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+divergent def list_nth_shared_mut_loop_pair_merge_loop_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  match h: ls0 with
+  | list_t.Cons x0 tl0 =>
+    match h: ls1 with
+    | list_t.Cons x1 tl1 =>
+      if i = (U32.ofInt 0 (by intlit))
+      then Result.ret (list_t.Cons ret0 tl1)
+      else
+        do
+          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let tl10 ←
+            list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
+
+/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+def list_nth_shared_mut_loop_pair_merge_back
+  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
+  Result (list_t T)
+  :=
+  list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
new file mode 100644
index 00000000..e14f9766
--- /dev/null
+++ b/tests/lean/Loops/Types.lean
@@ -0,0 +1,10 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [loops]: type definitions
+import Base
+open Primitives
+
+/- [loops::List] -/
+inductive list_t (T : Type) :=
+| Cons : T -> list_t T -> list_t T
+| Nil : list_t T
+
-- 
cgit v1.2.3


From b643bd00747e75d69b6066c55a1798b61277c4b6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 18:09:36 +0200
Subject: Regenerate the Lean test files

---
 tests/lean/Loops/Funs.lean  | 83 +++++++++++++++++++++++----------------------
 tests/lean/Loops/Types.lean |  5 ++-
 2 files changed, 47 insertions(+), 41 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 7d5f7595..9e084327 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -4,6 +4,8 @@ import Base
 import Loops.Types
 open Primitives
 
+namespace Loops
+
 /- [loops::sum] -/
 divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -68,7 +70,7 @@ def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
 
 /- [loops::list_mem] -/
 divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret true
@@ -82,7 +84,7 @@ def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool :=
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : U32) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -99,7 +101,7 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_back
   (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -118,7 +120,7 @@ def list_nth_mut_loop_back
 /- [loops::list_nth_shared_loop] -/
 divergent def list_nth_shared_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : U32) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -135,7 +137,7 @@ def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_fwd
   (x : Usize) (ls : list_t Usize) : Result Usize :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret y
@@ -152,7 +154,7 @@ def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_back
   (x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret (list_t.Cons ret0 tl)
@@ -176,7 +178,7 @@ def get_elem_mut_back
 /- [loops::get_elem_shared] -/
 divergent def get_elem_shared_loop_fwd
   (x : Usize) (ls : list_t Usize) : Result Usize :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret y
@@ -206,7 +208,7 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_fwd
   (T : Type) (i : U32) (ls : list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -226,7 +228,7 @@ def list_nth_mut_loop_with_id_fwd
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : U32) (ls : list_t T) (ret0 : T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -248,7 +250,7 @@ def list_nth_mut_loop_with_id_back
 /- [loops::list_nth_shared_loop_with_id] -/
 divergent def list_nth_shared_loop_with_id_loop_fwd
   (T : Type) (i : U32) (ls : list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -268,9 +270,9 @@ def list_nth_shared_loop_with_id_fwd
 /- [loops::list_nth_mut_loop_pair] -/
 divergent def list_nth_mut_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -291,9 +293,9 @@ divergent def list_nth_mut_loop_pair_loop_back'a
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -317,9 +319,9 @@ divergent def list_nth_mut_loop_pair_loop_back'b
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -341,9 +343,9 @@ def list_nth_mut_loop_pair_back'b
 /- [loops::list_nth_shared_loop_pair] -/
 divergent def list_nth_shared_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -362,9 +364,9 @@ def list_nth_shared_loop_pair_fwd
 /- [loops::list_nth_mut_loop_pair_merge] -/
 divergent def list_nth_mut_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -385,9 +387,9 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
   Result ((list_t T) × (list_t T))
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then
@@ -412,9 +414,9 @@ def list_nth_mut_loop_pair_merge_back
 /- [loops::list_nth_shared_loop_pair_merge] -/
 divergent def list_nth_shared_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -433,9 +435,9 @@ def list_nth_shared_loop_pair_merge_fwd
 /- [loops::list_nth_mut_shared_loop_pair] -/
 divergent def list_nth_mut_shared_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -456,9 +458,9 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -481,9 +483,9 @@ def list_nth_mut_shared_loop_pair_back
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -504,9 +506,9 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -529,9 +531,9 @@ def list_nth_mut_shared_loop_pair_merge_back
 /- [loops::list_nth_shared_mut_loop_pair] -/
 divergent def list_nth_shared_mut_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -552,9 +554,9 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -577,9 +579,9 @@ def list_nth_shared_mut_loop_pair_back
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -600,9 +602,9 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -622,3 +624,4 @@ def list_nth_shared_mut_loop_pair_merge_back
   :=
   list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
+end Loops
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index e14f9766..ca0403e9 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -3,8 +3,11 @@
 import Base
 open Primitives
 
+namespace Loops
+
 /- [loops::List] -/
 inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
 | Nil : list_t T
 
+end Loops
-- 
cgit v1.2.3


From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 tests/lean/Loops/Funs.lean  | 5 ++---
 tests/lean/Loops/Types.lean | 5 ++---
 2 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 9e084327..694f5450 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -3,8 +3,7 @@
 import Base
 import Loops.Types
 open Primitives
-
-namespace Loops
+namespace loops
 
 /- [loops::sum] -/
 divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
@@ -624,4 +623,4 @@ def list_nth_shared_mut_loop_pair_merge_back
   :=
   list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
-end Loops
+end loops
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index ca0403e9..5b5ed31f 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -2,12 +2,11 @@
 -- [loops]: type definitions
 import Base
 open Primitives
-
-namespace Loops
+namespace loops
 
 /- [loops::List] -/
 inductive list_t (T : Type) :=
 | Cons : T → list_t T → list_t T
 | Nil : list_t T
 
-end Loops
+end loops
-- 
cgit v1.2.3


From c07721dedb2cfe4c726c42606e623395cdfe5b80 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:09:07 +0200
Subject: Simplify the generated names for the types in Lean

---
 tests/lean/Loops/Funs.lean  | 355 ++++++++++++++++++++++----------------------
 tests/lean/Loops/Types.lean |   6 +-
 2 files changed, 178 insertions(+), 183 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 694f5450..383bc819 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -68,179 +68,175 @@ def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
   clear_loop_fwd_back v (Usize.ofInt 0 (by intlit))
 
 /- [loops::list_mem] -/
-divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool :=
+divergent def list_mem_loop_fwd (x : U32) (ls : List U32) : Result Bool :=
   match ls with
-  | list_t.Cons y tl =>
-    if y = x
-    then Result.ret true
-    else list_mem_loop_fwd x tl
-  | list_t.Nil => Result.ret false
+  | List.Cons y tl => if y = x
+                      then Result.ret true
+                      else list_mem_loop_fwd x tl
+  | List.Nil => Result.ret false
 
 /- [loops::list_mem] -/
-def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool :=
+def list_mem_fwd (x : U32) (ls : List U32) : Result Bool :=
   list_mem_loop_fwd x ls
 
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_fwd
-  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         list_nth_mut_loop_loop_fwd T tl i0
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop] -/
-def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
+def list_nth_mut_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T :=
   list_nth_mut_loop_loop_fwd T ls i
 
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_back
-  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
-    then Result.ret (list_t.Cons ret0 tl)
+    then Result.ret (List.Cons ret0 tl)
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
-        Result.ret (list_t.Cons x tl0)
-  | list_t.Nil => Result.fail Error.panic
+        Result.ret (List.Cons x tl0)
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop] -/
 def list_nth_mut_loop_back
-  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   list_nth_mut_loop_loop_back T ls i ret0
 
 /- [loops::list_nth_shared_loop] -/
 divergent def list_nth_shared_loop_loop_fwd
-  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         list_nth_shared_loop_loop_fwd T tl i0
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop] -/
-def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
+def list_nth_shared_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T :=
   list_nth_shared_loop_loop_fwd T ls i
 
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_fwd
-  (x : Usize) (ls : list_t Usize) : Result Usize :=
+  (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
-  | list_t.Cons y tl =>
+  | List.Cons y tl =>
     if y = x
     then Result.ret y
     else get_elem_mut_loop_fwd x tl
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::get_elem_mut] -/
-def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
+def get_elem_mut_fwd (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ←
-      vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
     get_elem_mut_loop_fwd x l
 
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_back
-  (x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) :=
+  (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
   match ls with
-  | list_t.Cons y tl =>
+  | List.Cons y tl =>
     if y = x
-    then Result.ret (list_t.Cons ret0 tl)
+    then Result.ret (List.Cons ret0 tl)
     else
       do
         let tl0 ← get_elem_mut_loop_back x tl ret0
-        Result.ret (list_t.Cons y tl0)
-  | list_t.Nil => Result.fail Error.panic
+        Result.ret (List.Cons y tl0)
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::get_elem_mut] -/
 def get_elem_mut_back
-  (slots : Vec (list_t Usize)) (x : Usize) (ret0 : Usize) :
-  Result (Vec (list_t Usize))
+  (slots : Vec (List Usize)) (x : Usize) (ret0 : Usize) :
+  Result (Vec (List Usize))
   :=
   do
-    let l ←
-      vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
     let l0 ← get_elem_mut_loop_back x l ret0
-    vec_index_mut_back (list_t Usize) slots (Usize.ofInt 0 (by intlit)) l0
+    vec_index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
 
 /- [loops::get_elem_shared] -/
 divergent def get_elem_shared_loop_fwd
-  (x : Usize) (ls : list_t Usize) : Result Usize :=
+  (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
-  | list_t.Cons y tl =>
+  | List.Cons y tl =>
     if y = x
     then Result.ret y
     else get_elem_shared_loop_fwd x tl
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::get_elem_shared] -/
 def get_elem_shared_fwd
-  (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
+  (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← vec_index_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← vec_index_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
     get_elem_shared_loop_fwd x l
 
 /- [loops::id_mut] -/
-def id_mut_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
+def id_mut_fwd (T : Type) (ls : List T) : Result (List T) :=
   Result.ret ls
 
 /- [loops::id_mut] -/
-def id_mut_back
-  (T : Type) (ls : list_t T) (ret0 : list_t T) : Result (list_t T) :=
+def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
   Result.ret ret0
 
 /- [loops::id_shared] -/
-def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
+def id_shared_fwd (T : Type) (ls : List T) : Result (List T) :=
   Result.ret ls
 
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_fwd
-  (T : Type) (i : U32) (ls : list_t T) : Result T :=
+  (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         list_nth_mut_loop_with_id_loop_fwd T i0 tl
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_with_id] -/
 def list_nth_mut_loop_with_id_fwd
-  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  (T : Type) (ls : List T) (i : U32) : Result T :=
   do
     let ls0 ← id_mut_fwd T ls
     list_nth_mut_loop_with_id_loop_fwd T i ls0
 
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_back
-  (T : Type) (i : U32) (ls : list_t T) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
-    then Result.ret (list_t.Cons ret0 tl)
+    then Result.ret (List.Cons ret0 tl)
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
-        Result.ret (list_t.Cons x tl0)
-  | list_t.Nil => Result.fail Error.panic
+        Result.ret (List.Cons x tl0)
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_with_id] -/
 def list_nth_mut_loop_with_id_back
-  (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   do
     let ls0 ← id_mut_fwd T ls
     let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0
@@ -248,378 +244,377 @@ def list_nth_mut_loop_with_id_back
 
 /- [loops::list_nth_shared_loop_with_id] -/
 divergent def list_nth_shared_loop_with_id_loop_fwd
-  (T : Type) (i : U32) (ls : list_t T) : Result T :=
+  (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
-  | list_t.Cons x tl =>
+  | List.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
         list_nth_shared_loop_with_id_loop_fwd T i0 tl
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop_with_id] -/
 def list_nth_shared_loop_with_id_fwd
-  (T : Type) (ls : list_t T) (i : U32) : Result T :=
+  (T : Type) (ls : List T) (i : U32) : Result T :=
   do
     let ls0 ← id_shared_fwd T ls
     list_nth_shared_loop_with_id_loop_fwd T i ls0
 
 /- [loops::list_nth_mut_loop_pair] -/
 divergent def list_nth_mut_loop_pair_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_pair] -/
 def list_nth_mut_loop_pair_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_mut_loop_pair_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair] -/
 divergent def list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl0)
+      then Result.ret (List.Cons ret0 tl0)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x0 tl00)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_pair] -/
 def list_nth_mut_loop_pair_back'a
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
 
 /- [loops::list_nth_mut_loop_pair] -/
 divergent def list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl1)
+      then Result.ret (List.Cons ret0 tl1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x1 tl10)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_pair] -/
 def list_nth_mut_loop_pair_back'b
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
 
 /- [loops::list_nth_shared_loop_pair] -/
 divergent def list_nth_shared_loop_pair_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop_pair] -/
 def list_nth_shared_loop_pair_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
 divergent def list_nth_mut_loop_pair_merge_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
 def list_nth_mut_loop_pair_merge_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
 divergent def list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
-  Result ((list_t T) × (list_t T))
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  Result ((List T) × (List T))
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then
-        let (t, t0) := ret0
-        Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1)
+      then let (t, t0) := ret0
+           Result.ret (List.Cons t tl0, List.Cons t0 tl1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let (tl00, tl10) ←
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x0 tl00, list_t.Cons x1 tl10)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
 def list_nth_mut_loop_pair_merge_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
-  Result ((list_t T) × (list_t T))
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+  Result ((List T) × (List T))
   :=
   list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
 /- [loops::list_nth_shared_loop_pair_merge] -/
 divergent def list_nth_shared_loop_pair_merge_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop_pair_merge] -/
 def list_nth_shared_loop_pair_merge_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
 divergent def list_nth_mut_shared_loop_pair_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
 def list_nth_mut_shared_loop_pair_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_mut_shared_loop_pair_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
 divergent def list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl0)
+      then Result.ret (List.Cons ret0 tl0)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x0 tl00)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
 def list_nth_mut_shared_loop_pair_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 def list_nth_mut_shared_loop_pair_merge_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_mut_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl0)
+      then Result.ret (List.Cons ret0 tl0)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x0 tl00)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x0 tl00)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 def list_nth_mut_shared_loop_pair_merge_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
 divergent def list_nth_shared_mut_loop_pair_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
 def list_nth_shared_mut_loop_pair_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_mut_loop_pair_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
 divergent def list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl1)
+      then Result.ret (List.Cons ret0 tl1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x1 tl10)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
 def list_nth_shared_mut_loop_pair_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 def list_nth_shared_mut_loop_pair_merge_fwd
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   match ls0 with
-  | list_t.Cons x0 tl0 =>
+  | List.Cons x0 tl0 =>
     match ls1 with
-    | list_t.Cons x1 tl1 =>
+    | List.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
-      then Result.ret (list_t.Cons ret0 tl1)
+      then Result.ret (List.Cons ret0 tl1)
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.Cons x1 tl10)
-    | list_t.Nil => Result.fail Error.panic
-  | list_t.Nil => Result.fail Error.panic
+          Result.ret (List.Cons x1 tl10)
+    | List.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 def list_nth_shared_mut_loop_pair_merge_back
-  (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
-  Result (list_t T)
+  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+  Result (List T)
   :=
   list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index 5b5ed31f..f8bc193b 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -5,8 +5,8 @@ open Primitives
 namespace loops
 
 /- [loops::List] -/
-inductive list_t (T : Type) :=
-| Cons : T → list_t T → list_t T
-| Nil : list_t T
+inductive List (T : Type) :=
+| Cons : T → List T → List T
+| Nil : List T
 
 end loops
-- 
cgit v1.2.3


From 5ca36bfc50083a01af2b7ae5f75993a520757ef5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:17:58 +0200
Subject: Simplify the names used in Primitives.lean

---
 tests/lean/Loops/Funs.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 383bc819..6e6eef3b 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -54,12 +54,12 @@ def sum_with_shared_borrows_fwd (max : U32) : Result U32 :=
 /- [loops::clear] -/
 divergent def clear_loop_fwd_back
   (v : Vec U32) (i : Usize) : Result (Vec U32) :=
-  let i0 := vec_len U32 v
+  let i0 := Vec.len U32 v
   if i < i0
   then
     do
       let i1 ← i + (Usize.ofInt 1 (by intlit))
-      let v0 ← vec_index_mut_back U32 v i (U32.ofInt 0 (by intlit))
+      let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit))
       clear_loop_fwd_back v0 i1
   else Result.ret v
 
@@ -145,7 +145,7 @@ divergent def get_elem_mut_loop_fwd
 /- [loops::get_elem_mut] -/
 def get_elem_mut_fwd (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
     get_elem_mut_loop_fwd x l
 
 /- [loops::get_elem_mut] -/
@@ -167,9 +167,9 @@ def get_elem_mut_back
   Result (Vec (List Usize))
   :=
   do
-    let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
     let l0 ← get_elem_mut_loop_back x l ret0
-    vec_index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
+    Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
 
 /- [loops::get_elem_shared] -/
 divergent def get_elem_shared_loop_fwd
@@ -185,7 +185,7 @@ divergent def get_elem_shared_loop_fwd
 def get_elem_shared_fwd
   (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← vec_index_fwd (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit))
     get_elem_shared_loop_fwd x l
 
 /- [loops::id_mut] -/
-- 
cgit v1.2.3


From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 12:20:28 +0200
Subject: Improve the generated comments

---
 tests/lean/Loops/Funs.lean | 300 ++++++++++++++++++++++-----------------------
 1 file changed, 148 insertions(+), 152 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 6e6eef3b..8cac7ac0 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -5,82 +5,83 @@ import Loops.Types
 open Primitives
 namespace loops
 
-/- [loops::sum] -/
-divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
+/- [loops::sum]: loop 0: forward function -/
+divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then
     do
       let s0 ← s + i
       let i0 ← i + (U32.ofInt 1 (by intlit))
-      sum_loop_fwd max i0 s0
+      sum_loop max i0 s0
   else s * (U32.ofInt 2 (by intlit))
 
-/- [loops::sum] -/
-def sum_fwd (max : U32) : Result U32 :=
-  sum_loop_fwd max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
+/- [loops::sum]: forward function -/
+def sum (max : U32) : Result U32 :=
+  sum_loop max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
 
-/- [loops::sum_with_mut_borrows] -/
-divergent def sum_with_mut_borrows_loop_fwd
+/- [loops::sum_with_mut_borrows]: loop 0: forward function -/
+divergent def sum_with_mut_borrows_loop
   (max : U32) (mi : U32) (ms : U32) : Result U32 :=
   if mi < max
   then
     do
       let ms0 ← ms + mi
       let mi0 ← mi + (U32.ofInt 1 (by intlit))
-      sum_with_mut_borrows_loop_fwd max mi0 ms0
+      sum_with_mut_borrows_loop max mi0 ms0
   else ms * (U32.ofInt 2 (by intlit))
 
-/- [loops::sum_with_mut_borrows] -/
-def sum_with_mut_borrows_fwd (max : U32) : Result U32 :=
-  sum_with_mut_borrows_loop_fwd max (U32.ofInt 0 (by intlit))
+/- [loops::sum_with_mut_borrows]: forward function -/
+def sum_with_mut_borrows (max : U32) : Result U32 :=
+  sum_with_mut_borrows_loop max (U32.ofInt 0 (by intlit))
     (U32.ofInt 0 (by intlit))
 
-/- [loops::sum_with_shared_borrows] -/
-divergent def sum_with_shared_borrows_loop_fwd
+/- [loops::sum_with_shared_borrows]: loop 0: forward function -/
+divergent def sum_with_shared_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then
     do
       let i0 ← i + (U32.ofInt 1 (by intlit))
       let s0 ← s + i0
-      sum_with_shared_borrows_loop_fwd max i0 s0
+      sum_with_shared_borrows_loop max i0 s0
   else s * (U32.ofInt 2 (by intlit))
 
-/- [loops::sum_with_shared_borrows] -/
-def sum_with_shared_borrows_fwd (max : U32) : Result U32 :=
-  sum_with_shared_borrows_loop_fwd max (U32.ofInt 0 (by intlit))
+/- [loops::sum_with_shared_borrows]: forward function -/
+def sum_with_shared_borrows (max : U32) : Result U32 :=
+  sum_with_shared_borrows_loop max (U32.ofInt 0 (by intlit))
     (U32.ofInt 0 (by intlit))
 
-/- [loops::clear] -/
-divergent def clear_loop_fwd_back
-  (v : Vec U32) (i : Usize) : Result (Vec U32) :=
+/- [loops::clear]: loop 0: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+divergent def clear_loop (v : Vec U32) (i : Usize) : Result (Vec U32) :=
   let i0 := Vec.len U32 v
   if i < i0
   then
     do
       let i1 ← i + (Usize.ofInt 1 (by intlit))
       let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit))
-      clear_loop_fwd_back v0 i1
+      clear_loop v0 i1
   else Result.ret v
 
-/- [loops::clear] -/
-def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
-  clear_loop_fwd_back v (Usize.ofInt 0 (by intlit))
+/- [loops::clear]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def clear (v : Vec U32) : Result (Vec U32) :=
+  clear_loop v (Usize.ofInt 0 (by intlit))
 
-/- [loops::list_mem] -/
-divergent def list_mem_loop_fwd (x : U32) (ls : List U32) : Result Bool :=
+/- [loops::list_mem]: loop 0: forward function -/
+divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
   match ls with
   | List.Cons y tl => if y = x
                       then Result.ret true
-                      else list_mem_loop_fwd x tl
+                      else list_mem_loop x tl
   | List.Nil => Result.ret false
 
-/- [loops::list_mem] -/
-def list_mem_fwd (x : U32) (ls : List U32) : Result Bool :=
-  list_mem_loop_fwd x ls
+/- [loops::list_mem]: forward function -/
+def list_mem (x : U32) (ls : List U32) : Result Bool :=
+  list_mem_loop x ls
 
-/- [loops::list_nth_mut_loop] -/
-divergent def list_nth_mut_loop_loop_fwd
+/- [loops::list_nth_mut_loop]: loop 0: forward function -/
+divergent def list_nth_mut_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
@@ -89,14 +90,14 @@ divergent def list_nth_mut_loop_loop_fwd
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_loop_fwd T tl i0
+        list_nth_mut_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop] -/
-def list_nth_mut_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T :=
-  list_nth_mut_loop_loop_fwd T ls i
+/- [loops::list_nth_mut_loop]: forward function -/
+def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T :=
+  list_nth_mut_loop_loop T ls i
 
-/- [loops::list_nth_mut_loop] -/
+/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/
 divergent def list_nth_mut_loop_loop_back
   (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match ls with
@@ -110,13 +111,13 @@ divergent def list_nth_mut_loop_loop_back
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop] -/
+/- [loops::list_nth_mut_loop]: backward function 0 -/
 def list_nth_mut_loop_back
   (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   list_nth_mut_loop_loop_back T ls i ret0
 
-/- [loops::list_nth_shared_loop] -/
-divergent def list_nth_shared_loop_loop_fwd
+/- [loops::list_nth_shared_loop]: loop 0: forward function -/
+divergent def list_nth_shared_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
@@ -125,30 +126,28 @@ divergent def list_nth_shared_loop_loop_fwd
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_shared_loop_loop_fwd T tl i0
+        list_nth_shared_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_loop] -/
-def list_nth_shared_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T :=
-  list_nth_shared_loop_loop_fwd T ls i
+/- [loops::list_nth_shared_loop]: forward function -/
+def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
+  list_nth_shared_loop_loop T ls i
 
-/- [loops::get_elem_mut] -/
-divergent def get_elem_mut_loop_fwd
-  (x : Usize) (ls : List Usize) : Result Usize :=
+/- [loops::get_elem_mut]: loop 0: forward function -/
+divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
-  | List.Cons y tl =>
-    if y = x
-    then Result.ret y
-    else get_elem_mut_loop_fwd x tl
+  | List.Cons y tl => if y = x
+                      then Result.ret y
+                      else get_elem_mut_loop x tl
   | List.Nil => Result.fail Error.panic
 
-/- [loops::get_elem_mut] -/
-def get_elem_mut_fwd (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
+/- [loops::get_elem_mut]: forward function -/
+def get_elem_mut (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
     let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
-    get_elem_mut_loop_fwd x l
+    get_elem_mut_loop x l
 
-/- [loops::get_elem_mut] -/
+/- [loops::get_elem_mut]: loop 0: backward function 0 -/
 divergent def get_elem_mut_loop_back
   (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
   match ls with
@@ -161,7 +160,7 @@ divergent def get_elem_mut_loop_back
         Result.ret (List.Cons y tl0)
   | List.Nil => Result.fail Error.panic
 
-/- [loops::get_elem_mut] -/
+/- [loops::get_elem_mut]: backward function 0 -/
 def get_elem_mut_back
   (slots : Vec (List Usize)) (x : Usize) (ret0 : Usize) :
   Result (Vec (List Usize))
@@ -171,37 +170,35 @@ def get_elem_mut_back
     let l0 ← get_elem_mut_loop_back x l ret0
     Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
 
-/- [loops::get_elem_shared] -/
-divergent def get_elem_shared_loop_fwd
+/- [loops::get_elem_shared]: loop 0: forward function -/
+divergent def get_elem_shared_loop
   (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
-  | List.Cons y tl =>
-    if y = x
-    then Result.ret y
-    else get_elem_shared_loop_fwd x tl
+  | List.Cons y tl => if y = x
+                      then Result.ret y
+                      else get_elem_shared_loop x tl
   | List.Nil => Result.fail Error.panic
 
-/- [loops::get_elem_shared] -/
-def get_elem_shared_fwd
-  (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
+/- [loops::get_elem_shared]: forward function -/
+def get_elem_shared (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
     let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit))
-    get_elem_shared_loop_fwd x l
+    get_elem_shared_loop x l
 
-/- [loops::id_mut] -/
-def id_mut_fwd (T : Type) (ls : List T) : Result (List T) :=
+/- [loops::id_mut]: forward function -/
+def id_mut (T : Type) (ls : List T) : Result (List T) :=
   Result.ret ls
 
-/- [loops::id_mut] -/
+/- [loops::id_mut]: backward function 0 -/
 def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
   Result.ret ret0
 
-/- [loops::id_shared] -/
-def id_shared_fwd (T : Type) (ls : List T) : Result (List T) :=
+/- [loops::id_shared]: forward function -/
+def id_shared (T : Type) (ls : List T) : Result (List T) :=
   Result.ret ls
 
-/- [loops::list_nth_mut_loop_with_id] -/
-divergent def list_nth_mut_loop_with_id_loop_fwd
+/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/
+divergent def list_nth_mut_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
@@ -210,17 +207,16 @@ divergent def list_nth_mut_loop_with_id_loop_fwd
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_with_id_loop_fwd T i0 tl
+        list_nth_mut_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_with_id] -/
-def list_nth_mut_loop_with_id_fwd
-  (T : Type) (ls : List T) (i : U32) : Result T :=
+/- [loops::list_nth_mut_loop_with_id]: forward function -/
+def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T :=
   do
-    let ls0 ← id_mut_fwd T ls
-    list_nth_mut_loop_with_id_loop_fwd T i ls0
+    let ls0 ← id_mut T ls
+    list_nth_mut_loop_with_id_loop T i ls0
 
-/- [loops::list_nth_mut_loop_with_id] -/
+/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/
 divergent def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
   match ls with
@@ -234,16 +230,16 @@ divergent def list_nth_mut_loop_with_id_loop_back
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_with_id] -/
+/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/
 def list_nth_mut_loop_with_id_back
   (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   do
-    let ls0 ← id_mut_fwd T ls
+    let ls0 ← id_mut T ls
     let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0
     id_mut_back T ls l
 
-/- [loops::list_nth_shared_loop_with_id] -/
-divergent def list_nth_shared_loop_with_id_loop_fwd
+/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/
+divergent def list_nth_shared_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
@@ -252,18 +248,18 @@ divergent def list_nth_shared_loop_with_id_loop_fwd
     else
       do
         let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_shared_loop_with_id_loop_fwd T i0 tl
+        list_nth_shared_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_loop_with_id] -/
-def list_nth_shared_loop_with_id_fwd
+/- [loops::list_nth_shared_loop_with_id]: forward function -/
+def list_nth_shared_loop_with_id
   (T : Type) (ls : List T) (i : U32) : Result T :=
   do
-    let ls0 ← id_shared_fwd T ls
-    list_nth_shared_loop_with_id_loop_fwd T i ls0
+    let ls0 ← id_shared T ls
+    list_nth_shared_loop_with_id_loop T i ls0
 
-/- [loops::list_nth_mut_loop_pair] -/
-divergent def list_nth_mut_loop_pair_loop_fwd
+/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/
+divergent def list_nth_mut_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -274,16 +270,16 @@ divergent def list_nth_mut_loop_pair_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
+          list_nth_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_pair] -/
-def list_nth_mut_loop_pair_fwd
+/- [loops::list_nth_mut_loop_pair]: forward function -/
+def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_loop_pair_loop_fwd T ls0 ls1 i
+  list_nth_mut_loop_pair_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_loop_pair] -/
+/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/
 divergent def list_nth_mut_loop_pair_loop_back'a
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -302,14 +298,14 @@ divergent def list_nth_mut_loop_pair_loop_back'a
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_pair] -/
+/- [loops::list_nth_mut_loop_pair]: backward function 0 -/
 def list_nth_mut_loop_pair_back'a
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
   :=
   list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
 
-/- [loops::list_nth_mut_loop_pair] -/
+/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/
 divergent def list_nth_mut_loop_pair_loop_back'b
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -328,15 +324,15 @@ divergent def list_nth_mut_loop_pair_loop_back'b
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_pair] -/
+/- [loops::list_nth_mut_loop_pair]: backward function 1 -/
 def list_nth_mut_loop_pair_back'b
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
   :=
   list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
 
-/- [loops::list_nth_shared_loop_pair] -/
-divergent def list_nth_shared_loop_pair_loop_fwd
+/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/
+divergent def list_nth_shared_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -347,17 +343,17 @@ divergent def list_nth_shared_loop_pair_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
+          list_nth_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_loop_pair] -/
-def list_nth_shared_loop_pair_fwd
+/- [loops::list_nth_shared_loop_pair]: forward function -/
+def list_nth_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_loop_pair_loop_fwd T ls0 ls1 i
+  list_nth_shared_loop_pair_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_loop_pair_merge] -/
-divergent def list_nth_mut_loop_pair_merge_loop_fwd
+/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_mut_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -368,16 +364,16 @@ divergent def list_nth_mut_loop_pair_merge_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
+          list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_pair_merge] -/
-def list_nth_mut_loop_pair_merge_fwd
+/- [loops::list_nth_mut_loop_pair_merge]: forward function -/
+def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
+  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_loop_pair_merge] -/
+/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/
 divergent def list_nth_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
   Result ((List T) × (List T))
@@ -398,15 +394,15 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_loop_pair_merge] -/
+/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/
 def list_nth_mut_loop_pair_merge_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
   Result ((List T) × (List T))
   :=
   list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
-/- [loops::list_nth_shared_loop_pair_merge] -/
-divergent def list_nth_shared_loop_pair_merge_loop_fwd
+/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_shared_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -417,17 +413,17 @@ divergent def list_nth_shared_loop_pair_merge_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
+          list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_loop_pair_merge] -/
-def list_nth_shared_loop_pair_merge_fwd
+/- [loops::list_nth_shared_loop_pair_merge]: forward function -/
+def list_nth_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
+  list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_shared_loop_pair] -/
-divergent def list_nth_mut_shared_loop_pair_loop_fwd
+/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/
+divergent def list_nth_mut_shared_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -438,16 +434,16 @@ divergent def list_nth_mut_shared_loop_pair_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
+          list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_shared_loop_pair] -/
-def list_nth_mut_shared_loop_pair_fwd
+/- [loops::list_nth_mut_shared_loop_pair]: forward function -/
+def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_shared_loop_pair_loop_fwd T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_shared_loop_pair] -/
+/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/
 divergent def list_nth_mut_shared_loop_pair_loop_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -467,15 +463,15 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_shared_loop_pair] -/
+/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/
 def list_nth_mut_shared_loop_pair_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
   :=
   list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
 
-/- [loops::list_nth_mut_shared_loop_pair_merge] -/
-divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
+/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_mut_shared_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -486,16 +482,16 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
+          list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_shared_loop_pair_merge] -/
-def list_nth_mut_shared_loop_pair_merge_fwd
+/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/
+def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_mut_shared_loop_pair_merge_loop_fwd T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
 
-/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -515,15 +511,15 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_mut_shared_loop_pair_merge] -/
+/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/
 def list_nth_mut_shared_loop_pair_merge_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
   :=
   list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
-/- [loops::list_nth_shared_mut_loop_pair] -/
-divergent def list_nth_shared_mut_loop_pair_loop_fwd
+/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/
+divergent def list_nth_shared_mut_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -534,16 +530,16 @@ divergent def list_nth_shared_mut_loop_pair_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
+          list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_mut_loop_pair] -/
-def list_nth_shared_mut_loop_pair_fwd
+/- [loops::list_nth_shared_mut_loop_pair]: forward function -/
+def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_mut_loop_pair_loop_fwd T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
 
-/- [loops::list_nth_shared_mut_loop_pair] -/
+/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/
 divergent def list_nth_shared_mut_loop_pair_loop_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -563,15 +559,15 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_mut_loop_pair] -/
+/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/
 def list_nth_shared_mut_loop_pair_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
   :=
   list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
 
-/- [loops::list_nth_shared_mut_loop_pair_merge] -/
-divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
+/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/
+divergent def list_nth_shared_mut_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
   | List.Cons x0 tl0 =>
@@ -582,16 +578,16 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
       else
         do
           let i0 ← i - (U32.ofInt 1 (by intlit))
-          list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
+          list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_mut_loop_pair_merge] -/
-def list_nth_shared_mut_loop_pair_merge_fwd
+/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/
+def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
-  list_nth_shared_mut_loop_pair_merge_loop_fwd T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
 
-/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
@@ -611,7 +607,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
 
-/- [loops::list_nth_shared_mut_loop_pair_merge] -/
+/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/
 def list_nth_shared_mut_loop_pair_merge_back
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
   Result (List T)
-- 
cgit v1.2.3


From e010c10fb9a1e2d88b52a4f6b4a0865448276013 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 15:58:38 +0200
Subject: Make the `by inlit` implicit

---
 tests/lean/Loops/Funs.lean | 140 ++++++++++++++++++++++-----------------------
 1 file changed, 67 insertions(+), 73 deletions(-)

(limited to 'tests/lean/Loops')

diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 8cac7ac0..f7e6603d 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -8,16 +8,15 @@ namespace loops
 /- [loops::sum]: loop 0: forward function -/
 divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
-  then
-    do
-      let s0 ← s + i
-      let i0 ← i + (U32.ofInt 1 (by intlit))
-      sum_loop max i0 s0
-  else s * (U32.ofInt 2 (by intlit))
+  then do
+         let s0 ← s + i
+         let i0 ← i + (U32.ofInt 1)
+         sum_loop max i0 s0
+  else s * (U32.ofInt 2)
 
 /- [loops::sum]: forward function -/
 def sum (max : U32) : Result U32 :=
-  sum_loop max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
+  sum_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::sum_with_mut_borrows]: loop 0: forward function -/
 divergent def sum_with_mut_borrows_loop
@@ -26,14 +25,13 @@ divergent def sum_with_mut_borrows_loop
   then
     do
       let ms0 ← ms + mi
-      let mi0 ← mi + (U32.ofInt 1 (by intlit))
+      let mi0 ← mi + (U32.ofInt 1)
       sum_with_mut_borrows_loop max mi0 ms0
-  else ms * (U32.ofInt 2 (by intlit))
+  else ms * (U32.ofInt 2)
 
 /- [loops::sum_with_mut_borrows]: forward function -/
 def sum_with_mut_borrows (max : U32) : Result U32 :=
-  sum_with_mut_borrows_loop max (U32.ofInt 0 (by intlit))
-    (U32.ofInt 0 (by intlit))
+  sum_with_mut_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::sum_with_shared_borrows]: loop 0: forward function -/
 divergent def sum_with_shared_borrows_loop
@@ -41,15 +39,14 @@ divergent def sum_with_shared_borrows_loop
   if i < max
   then
     do
-      let i0 ← i + (U32.ofInt 1 (by intlit))
+      let i0 ← i + (U32.ofInt 1)
       let s0 ← s + i0
       sum_with_shared_borrows_loop max i0 s0
-  else s * (U32.ofInt 2 (by intlit))
+  else s * (U32.ofInt 2)
 
 /- [loops::sum_with_shared_borrows]: forward function -/
 def sum_with_shared_borrows (max : U32) : Result U32 :=
-  sum_with_shared_borrows_loop max (U32.ofInt 0 (by intlit))
-    (U32.ofInt 0 (by intlit))
+  sum_with_shared_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::clear]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -58,15 +55,15 @@ divergent def clear_loop (v : Vec U32) (i : Usize) : Result (Vec U32) :=
   if i < i0
   then
     do
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
-      let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
+      let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0)
       clear_loop v0 i1
   else Result.ret v
 
 /- [loops::clear]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def clear (v : Vec U32) : Result (Vec U32) :=
-  clear_loop v (Usize.ofInt 0 (by intlit))
+  clear_loop v (Usize.ofInt 0)
 
 /- [loops::list_mem]: loop 0: forward function -/
 divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
@@ -85,12 +82,11 @@ divergent def list_nth_mut_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_loop T tl i0
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_mut_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop]: forward function -/
@@ -102,11 +98,11 @@ divergent def list_nth_mut_loop_loop_back
   (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -121,12 +117,11 @@ divergent def list_nth_shared_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_shared_loop_loop T tl i0
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_shared_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop]: forward function -/
@@ -144,7 +139,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
 /- [loops::get_elem_mut]: forward function -/
 def get_elem_mut (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
     get_elem_mut_loop x l
 
 /- [loops::get_elem_mut]: loop 0: backward function 0 -/
@@ -166,9 +161,9 @@ def get_elem_mut_back
   Result (Vec (List Usize))
   :=
   do
-    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
     let l0 ← get_elem_mut_loop_back x l ret0
-    Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
+    Vec.index_mut_back (List Usize) slots (Usize.ofInt 0) l0
 
 /- [loops::get_elem_shared]: loop 0: forward function -/
 divergent def get_elem_shared_loop
@@ -182,7 +177,7 @@ divergent def get_elem_shared_loop
 /- [loops::get_elem_shared]: forward function -/
 def get_elem_shared (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index (List Usize) slots (Usize.ofInt 0)
     get_elem_shared_loop x l
 
 /- [loops::id_mut]: forward function -/
@@ -202,12 +197,11 @@ divergent def list_nth_mut_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_with_id_loop T i0 tl
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_mut_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_with_id]: forward function -/
@@ -221,11 +215,11 @@ divergent def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -243,11 +237,11 @@ divergent def list_nth_shared_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         list_nth_shared_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
@@ -265,11 +259,11 @@ divergent def list_nth_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -288,11 +282,11 @@ divergent def list_nth_mut_loop_pair_loop_back'a
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
     | List.Nil => Result.fail Error.panic
@@ -314,11 +308,11 @@ divergent def list_nth_mut_loop_pair_loop_back'b
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
     | List.Nil => Result.fail Error.panic
@@ -338,11 +332,11 @@ divergent def list_nth_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -359,11 +353,11 @@ divergent def list_nth_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -382,12 +376,12 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then let (t, t0) := ret0
            Result.ret (List.Cons t tl0, List.Cons t0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let (tl00, tl10) ←
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
@@ -408,11 +402,11 @@ divergent def list_nth_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -429,11 +423,11 @@ divergent def list_nth_mut_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -452,11 +446,11 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ←
             list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
@@ -477,11 +471,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -500,11 +494,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ←
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
@@ -525,11 +519,11 @@ divergent def list_nth_shared_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -548,11 +542,11 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ←
             list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
@@ -573,11 +567,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -596,11 +590,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ←
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
-- 
cgit v1.2.3