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/Paper.lean | 125 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 125 insertions(+)
 create mode 100644 tests/lean/Paper.lean

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
new file mode 100644
index 00000000..9019b694
--- /dev/null
+++ b/tests/lean/Paper.lean
@@ -0,0 +1,125 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [paper]
+import Base
+open Primitives
+
+/- [paper::ref_incr] -/
+def ref_incr_fwd_back (x : I32) : Result I32 :=
+  x + (I32.ofInt 1 (by intlit))
+
+/- [paper::test_incr] -/
+def test_incr_fwd : Result Unit :=
+  do
+    let x ← ref_incr_fwd_back (I32.ofInt 0 (by intlit))
+    if not (x = (I32.ofInt 1 (by intlit)))
+    then Result.fail Error.panic
+    else Result.ret ()
+
+/- Unit test for [paper::test_incr] -/
+#assert (test_incr_fwd == .ret ())
+
+/- [paper::choose] -/
+def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
+  if b
+  then Result.ret x
+  else Result.ret y
+
+/- [paper::choose] -/
+def choose_back
+  (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
+  if b
+  then Result.ret (ret0, y)
+  else Result.ret (x, ret0)
+
+/- [paper::test_choose] -/
+def test_choose_fwd : Result Unit :=
+  do
+    let z ←
+      choose_fwd I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
+    let z0 ← z + (I32.ofInt 1 (by intlit))
+    if not (z0 = (I32.ofInt 1 (by intlit)))
+    then Result.fail Error.panic
+    else
+      do
+        let (x, y) ←
+          choose_back I32 true (I32.ofInt 0 (by intlit))
+            (I32.ofInt 0 (by intlit)) z0
+        if not (x = (I32.ofInt 1 (by intlit)))
+        then Result.fail Error.panic
+        else
+          if not (y = (I32.ofInt 0 (by intlit)))
+          then Result.fail Error.panic
+          else Result.ret ()
+
+/- Unit test for [paper::test_choose] -/
+#assert (test_choose_fwd == .ret ())
+
+/- [paper::List] -/
+inductive list_t (T : Type) :=
+| Cons : T -> list_t T -> list_t T
+| Nil : list_t T
+
+/- [paper::list_nth_mut] -/
+divergent def list_nth_mut_fwd
+  (T : Type) (l : list_t T) (i : U32) : Result T :=
+  match h: l 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_fwd T tl i0
+  | list_t.Nil => Result.fail Error.panic
+
+/- [paper::list_nth_mut] -/
+divergent def list_nth_mut_back
+  (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  match h: l 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_back T tl i0 ret0
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
+
+/- [paper::sum] -/
+divergent def sum_fwd (l : list_t I32) : Result I32 :=
+  match h: l with
+  | list_t.Cons x tl => do
+                          let i ← sum_fwd tl
+                          x + i
+  | list_t.Nil => Result.ret (I32.ofInt 0 (by intlit))
+
+/- [paper::test_nth] -/
+def test_nth_fwd : Result Unit :=
+  do
+    let l := list_t.Nil
+    let l0 := list_t.Cons (I32.ofInt 3 (by intlit)) l
+    let l1 := list_t.Cons (I32.ofInt 2 (by intlit)) l0
+    let x ←
+      list_nth_mut_fwd I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1)
+        (U32.ofInt 2 (by intlit))
+    let x0 ← x + (I32.ofInt 1 (by intlit))
+    let l2 ←
+      list_nth_mut_back I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1)
+        (U32.ofInt 2 (by intlit)) x0
+    let i ← sum_fwd l2
+    if not (i = (I32.ofInt 7 (by intlit)))
+    then Result.fail Error.panic
+    else Result.ret ()
+
+/- Unit test for [paper::test_nth] -/
+#assert (test_nth_fwd == .ret ())
+
+/- [paper::call_choose] -/
+def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
+  do
+    let (px, py) := p
+    let pz ← choose_fwd U32 true px py
+    let pz0 ← pz + (U32.ofInt 1 (by intlit))
+    let (px0, _) ← choose_back U32 true px py pz0
+    Result.ret px0
+
-- 
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/Paper.lean | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 9019b694..edcb5c1b 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -3,6 +3,8 @@
 import Base
 open Primitives
 
+namespace Paper
+
 /- [paper::ref_incr] -/
 def ref_incr_fwd_back (x : I32) : Result I32 :=
   x + (I32.ofInt 1 (by intlit))
@@ -56,13 +58,13 @@ def test_choose_fwd : Result Unit :=
 
 /- [paper::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
 
 /- [paper::list_nth_mut] -/
 divergent def list_nth_mut_fwd
   (T : Type) (l : list_t T) (i : U32) : Result T :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -74,7 +76,7 @@ divergent def list_nth_mut_fwd
 /- [paper::list_nth_mut] -/
 divergent def list_nth_mut_back
   (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -87,7 +89,7 @@ divergent def list_nth_mut_back
 
 /- [paper::sum] -/
 divergent def sum_fwd (l : list_t I32) : Result I32 :=
-  match h: l with
+  match l with
   | list_t.Cons x tl => do
                           let i ← sum_fwd tl
                           x + i
@@ -123,3 +125,4 @@ def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
 
+end Paper
-- 
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/Paper.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index edcb5c1b..c34941ef 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -2,8 +2,7 @@
 -- [paper]
 import Base
 open Primitives
-
-namespace Paper
+namespace paper
 
 /- [paper::ref_incr] -/
 def ref_incr_fwd_back (x : I32) : Result I32 :=
@@ -125,4 +124,4 @@ def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
 
-end Paper
+end paper
-- 
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/Paper.lean | 43 +++++++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 22 deletions(-)

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index c34941ef..9f63b460 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -56,56 +56,55 @@ def test_choose_fwd : Result Unit :=
 #assert (test_choose_fwd == .ret ())
 
 /- [paper::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
 
 /- [paper::list_nth_mut] -/
-divergent def list_nth_mut_fwd
-  (T : Type) (l : list_t T) (i : U32) : Result T :=
+divergent def list_nth_mut_fwd (T : Type) (l : List T) (i : U32) : Result T :=
   match l 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_fwd T tl i0
-  | list_t.Nil => Result.fail Error.panic
+  | List.Nil => Result.fail Error.panic
 
 /- [paper::list_nth_mut] -/
 divergent def list_nth_mut_back
-  (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match l 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_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
 
 /- [paper::sum] -/
-divergent def sum_fwd (l : list_t I32) : Result I32 :=
+divergent def sum_fwd (l : List I32) : Result I32 :=
   match l with
-  | list_t.Cons x tl => do
-                          let i ← sum_fwd tl
-                          x + i
-  | list_t.Nil => Result.ret (I32.ofInt 0 (by intlit))
+  | List.Cons x tl => do
+                        let i ← sum_fwd tl
+                        x + i
+  | List.Nil => Result.ret (I32.ofInt 0 (by intlit))
 
 /- [paper::test_nth] -/
 def test_nth_fwd : Result Unit :=
   do
-    let l := list_t.Nil
-    let l0 := list_t.Cons (I32.ofInt 3 (by intlit)) l
-    let l1 := list_t.Cons (I32.ofInt 2 (by intlit)) l0
+    let l := List.Nil
+    let l0 := List.Cons (I32.ofInt 3 (by intlit)) l
+    let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0
     let x ←
-      list_nth_mut_fwd I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1)
+      list_nth_mut_fwd I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
         (U32.ofInt 2 (by intlit))
     let x0 ← x + (I32.ofInt 1 (by intlit))
     let l2 ←
-      list_nth_mut_back I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1)
+      list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
         (U32.ofInt 2 (by intlit)) x0
     let i ← sum_fwd l2
     if not (i = (I32.ofInt 7 (by intlit)))
-- 
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/Paper.lean | 57 ++++++++++++++++++++++++++-------------------------
 1 file changed, 29 insertions(+), 28 deletions(-)

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 9f63b460..ade65656 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -4,39 +4,40 @@ import Base
 open Primitives
 namespace paper
 
-/- [paper::ref_incr] -/
-def ref_incr_fwd_back (x : I32) : Result I32 :=
+/- [paper::ref_incr]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def ref_incr (x : I32) : Result I32 :=
   x + (I32.ofInt 1 (by intlit))
 
-/- [paper::test_incr] -/
-def test_incr_fwd : Result Unit :=
+/- [paper::test_incr]: forward function -/
+def test_incr : Result Unit :=
   do
-    let x ← ref_incr_fwd_back (I32.ofInt 0 (by intlit))
+    let x ← ref_incr (I32.ofInt 0 (by intlit))
     if not (x = (I32.ofInt 1 (by intlit)))
     then Result.fail Error.panic
     else Result.ret ()
 
 /- Unit test for [paper::test_incr] -/
-#assert (test_incr_fwd == .ret ())
+#assert (test_incr == .ret ())
 
-/- [paper::choose] -/
-def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
+/- [paper::choose]: forward function -/
+def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
   if b
   then Result.ret x
   else Result.ret y
 
-/- [paper::choose] -/
+/- [paper::choose]: backward function 0 -/
 def choose_back
   (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
   if b
   then Result.ret (ret0, y)
   else Result.ret (x, ret0)
 
-/- [paper::test_choose] -/
-def test_choose_fwd : Result Unit :=
+/- [paper::test_choose]: forward function -/
+def test_choose : Result Unit :=
   do
     let z ←
-      choose_fwd I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
+      choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
     let z0 ← z + (I32.ofInt 1 (by intlit))
     if not (z0 = (I32.ofInt 1 (by intlit)))
     then Result.fail Error.panic
@@ -53,25 +54,25 @@ def test_choose_fwd : Result Unit :=
           else Result.ret ()
 
 /- Unit test for [paper::test_choose] -/
-#assert (test_choose_fwd == .ret ())
+#assert (test_choose == .ret ())
 
 /- [paper::List] -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
-/- [paper::list_nth_mut] -/
-divergent def list_nth_mut_fwd (T : Type) (l : List T) (i : U32) : Result T :=
+/- [paper::list_nth_mut]: forward function -/
+divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | 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_fwd T tl i0
+           list_nth_mut T tl i0
   | List.Nil => Result.fail Error.panic
 
-/- [paper::list_nth_mut] -/
+/- [paper::list_nth_mut]: backward function 0 -/
 divergent def list_nth_mut_back
   (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match l with
@@ -85,40 +86,40 @@ divergent def list_nth_mut_back
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
 
-/- [paper::sum] -/
-divergent def sum_fwd (l : List I32) : Result I32 :=
+/- [paper::sum]: forward function -/
+divergent def sum (l : List I32) : Result I32 :=
   match l with
   | List.Cons x tl => do
-                        let i ← sum_fwd tl
+                        let i ← sum tl
                         x + i
   | List.Nil => Result.ret (I32.ofInt 0 (by intlit))
 
-/- [paper::test_nth] -/
-def test_nth_fwd : Result Unit :=
+/- [paper::test_nth]: forward function -/
+def test_nth : Result Unit :=
   do
     let l := List.Nil
     let l0 := List.Cons (I32.ofInt 3 (by intlit)) l
     let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0
     let x ←
-      list_nth_mut_fwd I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
+      list_nth_mut I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
         (U32.ofInt 2 (by intlit))
     let x0 ← x + (I32.ofInt 1 (by intlit))
     let l2 ←
       list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
         (U32.ofInt 2 (by intlit)) x0
-    let i ← sum_fwd l2
+    let i ← sum l2
     if not (i = (I32.ofInt 7 (by intlit)))
     then Result.fail Error.panic
     else Result.ret ()
 
 /- Unit test for [paper::test_nth] -/
-#assert (test_nth_fwd == .ret ())
+#assert (test_nth == .ret ())
 
-/- [paper::call_choose] -/
-def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
+/- [paper::call_choose]: forward function -/
+def call_choose (p : (U32 × U32)) : Result U32 :=
   do
     let (px, py) := p
-    let pz ← choose_fwd U32 true px py
+    let pz ← choose U32 true px py
     let pz0 ← pz + (U32.ofInt 1 (by intlit))
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
-- 
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/Paper.lean | 48 +++++++++++++++++++++---------------------------
 1 file changed, 21 insertions(+), 27 deletions(-)

(limited to 'tests/lean/Paper.lean')

diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index ade65656..cee7128a 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -7,13 +7,13 @@ namespace paper
 /- [paper::ref_incr]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def ref_incr (x : I32) : Result I32 :=
-  x + (I32.ofInt 1 (by intlit))
+  x + (I32.ofInt 1)
 
 /- [paper::test_incr]: forward function -/
 def test_incr : Result Unit :=
   do
-    let x ← ref_incr (I32.ofInt 0 (by intlit))
-    if not (x = (I32.ofInt 1 (by intlit)))
+    let x ← ref_incr (I32.ofInt 0)
+    if not (x = (I32.ofInt 1))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -36,20 +36,17 @@ def choose_back
 /- [paper::test_choose]: forward function -/
 def test_choose : Result Unit :=
   do
-    let z ←
-      choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
-    let z0 ← z + (I32.ofInt 1 (by intlit))
-    if not (z0 = (I32.ofInt 1 (by intlit)))
+    let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0)
+    let z0 ← z + (I32.ofInt 1)
+    if not (z0 = (I32.ofInt 1))
     then Result.fail Error.panic
     else
       do
-        let (x, y) ←
-          choose_back I32 true (I32.ofInt 0 (by intlit))
-            (I32.ofInt 0 (by intlit)) z0
-        if not (x = (I32.ofInt 1 (by intlit)))
+        let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0
+        if not (x = (I32.ofInt 1))
         then Result.fail Error.panic
         else
-          if not (y = (I32.ofInt 0 (by intlit)))
+          if not (y = (I32.ofInt 0))
           then Result.fail Error.panic
           else Result.ret ()
 
@@ -65,10 +62,10 @@ inductive List (T : Type) :=
 divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
   match l 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_mut T tl i0
   | List.Nil => Result.fail Error.panic
 
@@ -77,11 +74,11 @@ divergent def list_nth_mut_back
   (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match l 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_back T tl i0 ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -92,23 +89,20 @@ divergent def sum (l : List I32) : Result I32 :=
   | List.Cons x tl => do
                         let i ← sum tl
                         x + i
-  | List.Nil => Result.ret (I32.ofInt 0 (by intlit))
+  | List.Nil => Result.ret (I32.ofInt 0)
 
 /- [paper::test_nth]: forward function -/
 def test_nth : Result Unit :=
   do
     let l := List.Nil
-    let l0 := List.Cons (I32.ofInt 3 (by intlit)) l
-    let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0
-    let x ←
-      list_nth_mut I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
-        (U32.ofInt 2 (by intlit))
-    let x0 ← x + (I32.ofInt 1 (by intlit))
+    let l0 := List.Cons (I32.ofInt 3) l
+    let l1 := List.Cons (I32.ofInt 2) l0
+    let x ← list_nth_mut I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2)
+    let x0 ← x + (I32.ofInt 1)
     let l2 ←
-      list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
-        (U32.ofInt 2 (by intlit)) x0
+      list_nth_mut_back I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2) x0
     let i ← sum l2
-    if not (i = (I32.ofInt 7 (by intlit)))
+    if not (i = (I32.ofInt 7))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -120,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
   do
     let (px, py) := p
     let pz ← choose U32 true px py
-    let pz0 ← pz + (U32.ofInt 1 (by intlit))
+    let pz0 ← pz + (U32.ofInt 1)
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
 
-- 
cgit v1.2.3