From 14aed083b850c2d8a77cfe394827aeecce06514b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 8 Mar 2023 00:39:05 +0100
Subject: Improve the generation of variant names for Lean

---
 tests/lean/misc-polonius_list/PoloniusList.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'tests/lean/misc-polonius_list')

diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean
index d679230d..a3bbfd0a 100644
--- a/tests/lean/misc-polonius_list/PoloniusList.lean
+++ b/tests/lean/misc-polonius_list/PoloniusList.lean
@@ -6,18 +6,18 @@ structure OpaqueDefs where
   
   /- [polonius_list::List] -/
   inductive list_t (T : Type) :=
-  | ListCons : T -> list_t T -> list_t T
-  | ListNil : list_t T
+  | Cons : T -> list_t T -> list_t T
+  | Nil : list_t T
   
   /- [polonius_list::get_list_at_x] -/
   def get_list_at_x_fwd
     (ls : list_t UInt32) (x : UInt32) : Result (list_t UInt32) :=
     match h: ls with
-    | list_t.ListCons hd tl =>
+    | list_t.Cons hd tl =>
       if h: hd = x
-      then Result.ret (list_t.ListCons hd tl)
+      then Result.ret (list_t.Cons hd tl)
       else get_list_at_x_fwd tl x
-    | list_t.ListNil => Result.ret list_t.ListNil
+    | list_t.Nil => Result.ret list_t.Nil
   
   /- [polonius_list::get_list_at_x] -/
   def get_list_at_x_back
@@ -25,12 +25,12 @@ structure OpaqueDefs where
     Result (list_t UInt32)
     :=
     match h: ls with
-    | list_t.ListCons hd tl =>
+    | list_t.Cons hd tl =>
       if h: hd = x
       then Result.ret ret0
       else
         do
           let tl0 ← get_list_at_x_back tl x ret0
-          Result.ret (list_t.ListCons hd tl0)
-    | list_t.ListNil => Result.ret ret0
+          Result.ret (list_t.Cons hd tl0)
+    | list_t.Nil => Result.ret ret0
   
-- 
cgit v1.2.3