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

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

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
new file mode 100644
index 00000000..671f54ea
--- /dev/null
+++ b/tests/lean/PoloniusList.lean
@@ -0,0 +1,33 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [polonius_list]
+import Base
+open Primitives
+
+/- [polonius_list::List] -/
+inductive list_t (T : Type) :=
+| Cons : T -> list_t T -> list_t T
+| Nil : list_t T
+
+/- [polonius_list::get_list_at_x] -/
+divergent def get_list_at_x_fwd
+  (ls : list_t U32) (x : U32) : Result (list_t U32) :=
+  match h: ls with
+  | list_t.Cons hd tl =>
+    if hd = x
+    then Result.ret (list_t.Cons hd tl)
+    else get_list_at_x_fwd tl x
+  | list_t.Nil => Result.ret list_t.Nil
+
+/- [polonius_list::get_list_at_x] -/
+divergent def get_list_at_x_back
+  (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) :=
+  match h: ls with
+  | list_t.Cons hd tl =>
+    if hd = x
+    then Result.ret ret0
+    else
+      do
+        let tl0 ← get_list_at_x_back tl x ret0
+        Result.ret (list_t.Cons hd tl0)
+  | list_t.Nil => Result.ret ret0
+
-- 
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/PoloniusList.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

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

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 671f54ea..0f2a05e3 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -3,15 +3,17 @@
 import Base
 open Primitives
 
+namespace PoloniusList
+
 /- [polonius_list::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
 
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_fwd
   (ls : list_t U32) (x : U32) : Result (list_t U32) :=
-  match h: ls with
+  match ls with
   | list_t.Cons hd tl =>
     if hd = x
     then Result.ret (list_t.Cons hd tl)
@@ -21,7 +23,7 @@ divergent def get_list_at_x_fwd
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_back
   (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) :=
-  match h: ls with
+  match ls with
   | list_t.Cons hd tl =>
     if hd = x
     then Result.ret ret0
@@ -31,3 +33,4 @@ divergent def get_list_at_x_back
         Result.ret (list_t.Cons hd tl0)
   | list_t.Nil => Result.ret ret0
 
+end PoloniusList
-- 
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/PoloniusList.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 0f2a05e3..0ff01b47 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -2,8 +2,7 @@
 -- [polonius_list]
 import Base
 open Primitives
-
-namespace PoloniusList
+namespace polonius_list
 
 /- [polonius_list::List] -/
 inductive list_t (T : Type) :=
@@ -33,4 +32,4 @@ divergent def get_list_at_x_back
         Result.ret (list_t.Cons hd tl0)
   | list_t.Nil => Result.ret ret0
 
-end PoloniusList
+end polonius_list
-- 
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/PoloniusList.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

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

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 0ff01b47..1d7ec99b 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -5,31 +5,31 @@ open Primitives
 namespace polonius_list
 
 /- [polonius_list::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
 
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_fwd
-  (ls : list_t U32) (x : U32) : Result (list_t U32) :=
+  (ls : List U32) (x : U32) : Result (List U32) :=
   match ls with
-  | list_t.Cons hd tl =>
+  | List.Cons hd tl =>
     if hd = x
-    then Result.ret (list_t.Cons hd tl)
+    then Result.ret (List.Cons hd tl)
     else get_list_at_x_fwd tl x
-  | list_t.Nil => Result.ret list_t.Nil
+  | List.Nil => Result.ret List.Nil
 
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_back
-  (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) :=
+  (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
   match ls with
-  | list_t.Cons hd tl =>
+  | List.Cons hd tl =>
     if hd = x
     then Result.ret ret0
     else
       do
         let tl0 ← get_list_at_x_back tl x ret0
-        Result.ret (list_t.Cons hd tl0)
-  | list_t.Nil => Result.ret ret0
+        Result.ret (List.Cons hd tl0)
+  | List.Nil => Result.ret ret0
 
 end polonius_list
-- 
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/PoloniusList.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

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

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 1d7ec99b..1453c275 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -9,17 +9,16 @@ inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
-/- [polonius_list::get_list_at_x] -/
-divergent def get_list_at_x_fwd
-  (ls : List U32) (x : U32) : Result (List U32) :=
+/- [polonius_list::get_list_at_x]: forward function -/
+divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
   match ls with
   | List.Cons hd tl =>
     if hd = x
     then Result.ret (List.Cons hd tl)
-    else get_list_at_x_fwd tl x
+    else get_list_at_x tl x
   | List.Nil => Result.ret List.Nil
 
-/- [polonius_list::get_list_at_x] -/
+/- [polonius_list::get_list_at_x]: backward function 0 -/
 divergent def get_list_at_x_back
   (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
   match ls with
-- 
cgit v1.2.3