Improve the generation of variant names for Lean

5 files changed, 173 insertions, 176 deletions

diff --git a/tests/lean/misc-loops/Loops/Funs.lean b/tests/lean/misc-loops/Loops/Funs.lean
index 5a81ebff..f79a27a9 100644
--- a/tests/lean/misc-loops/Loops/Funs.lean
+++ b/tests/lean/misc-loops/Loops/Funs.lean
@@ -79,11 +79,11 @@ def clear_fwd_back (v : Vec UInt32) : Result (Vec UInt32) :=
 /- [loops::list_mem] -/
 def list_mem_loop_fwd (x : UInt32) (ls : list_t UInt32) : (Result Bool) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret true
     else list_mem_loop_fwd x tl
-  | list_t.ListNil => Result.ret false
+  | list_t.Nil => Result.ret false
 termination_by list_mem_loop_fwd x ls => list_mem_loop_terminates x ls
 decreasing_by list_mem_loop_decreases x ls
 
@@ -95,14 +95,14 @@ def list_mem_fwd (x : UInt32) (ls : list_t UInt32) : Result Bool :=
 def list_nth_mut_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : UInt32) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_loop_fwd T tl i0
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_loop_fwd ls i =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -115,15 +115,15 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : UInt32) : Result T :=
 def list_nth_mut_loop_loop_back
   (T : Type) (ls : list_t T) (i : UInt32) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
-        Result.ret (list_t.ListCons x tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_loop_back ls i ret0 =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -137,14 +137,14 @@ def list_nth_mut_loop_back
 def list_nth_shared_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : UInt32) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_loop_fwd T tl i0
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_loop_fwd ls i =>
   list_nth_shared_loop_loop_terminates T ls i
 decreasing_by list_nth_shared_loop_loop_decreases ls i
@@ -157,11 +157,11 @@ def list_nth_shared_loop_fwd
 /- [loops::get_elem_mut] -/
 def get_elem_mut_loop_fwd (x : USize) (ls : list_t USize) : (Result USize) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret y
     else get_elem_mut_loop_fwd x tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_mut_loop_fwd x ls => get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
 
@@ -176,14 +176,14 @@ def get_elem_mut_fwd (slots : Vec (list_t USize)) (x : USize) : Result USize :=
 def get_elem_mut_loop_back
   (x : USize) (ls : list_t USize) (ret0 : USize) : (Result (list_t USize)) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let tl0 ← get_elem_mut_loop_back x tl ret0
-        Result.ret (list_t.ListCons y tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons y tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_mut_loop_back x ls ret0 =>
   get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
@@ -203,11 +203,11 @@ def get_elem_mut_back
 def get_elem_shared_loop_fwd
   (x : USize) (ls : list_t USize) : (Result USize) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret y
     else get_elem_shared_loop_fwd x tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_shared_loop_fwd x ls =>
   get_elem_shared_loop_terminates x ls
 decreasing_by get_elem_shared_loop_decreases x ls
@@ -237,14 +237,14 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
 def list_nth_mut_loop_with_id_loop_fwd
   (T : Type) (i : UInt32) (ls : list_t T) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_with_id_loop_fwd T i0 tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_with_id_loop_fwd i ls =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -260,15 +260,15 @@ def list_nth_mut_loop_with_id_fwd
 def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : UInt32) (ls : list_t T) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
-        Result.ret (list_t.ListCons x tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -285,14 +285,14 @@ def list_nth_mut_loop_with_id_back
 def list_nth_shared_loop_with_id_loop_fwd
   (T : Type) (i : UInt32) (ls : list_t T) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_with_id_loop_fwd T i0 tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_with_id_loop_fwd i ls =>
   list_nth_shared_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls
@@ -310,17 +310,17 @@ def list_nth_mut_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -338,18 +338,18 @@ def list_nth_mut_loop_pair_loop_back'a
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -367,18 +367,18 @@ def list_nth_mut_loop_pair_loop_back'b
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -396,17 +396,17 @@ def list_nth_shared_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -424,17 +424,17 @@ def list_nth_mut_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -452,21 +452,21 @@ def list_nth_mut_loop_pair_merge_loop_back
   (Result ((list_t T) × (list_t T)))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then
         let (t, t0) := ret0
-        Result.ret (list_t.ListCons t tl0, list_t.ListCons t0 tl1)
+        Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let (tl00, tl10) ←
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00, list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          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
 termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -484,17 +484,17 @@ def list_nth_shared_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -512,17 +512,17 @@ def list_nth_mut_shared_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -540,19 +540,19 @@ def list_nth_mut_shared_loop_pair_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -570,17 +570,17 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -598,19 +598,19 @@ def list_nth_mut_shared_loop_pair_merge_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -628,17 +628,17 @@ def list_nth_shared_mut_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -656,19 +656,19 @@ def list_nth_shared_mut_loop_pair_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -686,17 +686,17 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -714,19 +714,19 @@ def list_nth_shared_mut_loop_pair_merge_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
diff --git a/tests/lean/misc-loops/Loops/Types.lean b/tests/lean/misc-loops/Loops/Types.lean
index f4b6809e..ca43f4c8 100644
--- a/tests/lean/misc-loops/Loops/Types.lean
+++ b/tests/lean/misc-loops/Loops/Types.lean
@@ -4,6 +4,6 @@ import Base.Primitives
 
 /- [loops::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
 
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
index 12d4190c..e2697385 100644
--- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
@@ -11,29 +11,29 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::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
   
   /- [no_nested_borrows::One] -/
   inductive one_t (T1 : Type) :=
-  | OneOne : T1 -> one_t T1
+  | One : T1 -> one_t T1
   
   /- [no_nested_borrows::EmptyEnum] -/
   inductive empty_enum_t :=
-  | EmptyEnumEmpty : empty_enum_t
+  | Empty : empty_enum_t
   
   /- [no_nested_borrows::Enum] -/
   inductive enum_t :=
-  | EnumVariant1 : enum_t
-  | EnumVariant2 : enum_t
+  | Variant1 : enum_t
+  | Variant2 : enum_t
   
   /- [no_nested_borrows::EmptyStruct] -/
   structure empty_struct_t where
   
   /- [no_nested_borrows::Sum] -/
   inductive sum_t (T1 T2 : Type) :=
-  | SumLeft : T1 -> sum_t T1 T2
-  | SumRight : T2 -> sum_t T1 T2
+  | Left : T1 -> sum_t T1 T2
+  | Right : T2 -> sum_t T1 T2
   
   /- [no_nested_borrows::neg_test] -/
   def neg_test_fwd (x : Int32) : Result Int32 :=
@@ -187,15 +187,15 @@ structure OpaqueDefs where
   /- [no_nested_borrows::is_cons] -/
   def is_cons_fwd (T : Type) (l : list_t T) : Result Bool :=
     match h: l with
-    | list_t.ListCons t l0 => Result.ret true
-    | list_t.ListNil => Result.ret false
+    | list_t.Cons t l0 => Result.ret true
+    | list_t.Nil => Result.ret false
   
   /- [no_nested_borrows::test_is_cons] -/
   def test_is_cons_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
+      let l := list_t.Nil
       let b ←
-        is_cons_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) l)
+        is_cons_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l)
       if h: not b
       then Result.fail Error.panic
       else Result.ret ()
@@ -206,16 +206,15 @@ structure OpaqueDefs where
   /- [no_nested_borrows::split_list] -/
   def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) :=
     match h: l with
-    | list_t.ListCons hd tl => Result.ret (hd, tl)
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Cons hd tl => Result.ret (hd, tl)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::test_split_list] -/
   def test_split_list_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
+      let l := list_t.Nil
       let p ←
-        split_list_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit))
-          l)
+        split_list_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l)
       let (hd, _) := p
       if h: not (hd = (Int32.ofNatCore 0 (by intlit)))
       then Result.fail Error.panic
@@ -267,88 +266,87 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::NodeElem] -/
   mutual inductive node_elem_t (T : Type) :=
-  | NodeElemCons : tree_t T -> node_elem_t T -> node_elem_t T
-  | NodeElemNil : node_elem_t T
+  | Cons : tree_t T -> node_elem_t T -> node_elem_t T
+  | Nil : node_elem_t T
   
   /- [no_nested_borrows::Tree] -/
   inductive tree_t (T : Type) :=
-  | TreeLeaf : T -> tree_t T
-  | TreeNode : T -> node_elem_t T -> tree_t T -> tree_t T
+  | Leaf : T -> tree_t T
+  | Node : T -> node_elem_t T -> tree_t T -> tree_t T
   
   /- [no_nested_borrows::list_length] -/
   def list_length_fwd (T : Type) (l : list_t T) : Result UInt32 :=
     match h: l with
-    | list_t.ListCons t l1 =>
+    | list_t.Cons t l1 =>
       do
         let i ← list_length_fwd T l1
         UInt32.checked_add (UInt32.ofNatCore 1 (by intlit)) i
-    | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit))
+    | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit))
   
   /- [no_nested_borrows::list_nth_shared] -/
   def list_nth_shared_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_back
     (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl)
+      then Result.ret (list_t.Cons ret0 tl)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl0 ← list_nth_mut_back T tl i0 ret0
-          Result.ret (list_t.ListCons x tl0)
-    | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x tl0)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_rev_aux] -/
   def list_rev_aux_fwd
     (T : Type) (li : list_t T) (lo : list_t T) : Result (list_t T) :=
     match h: li with
-    | list_t.ListCons hd tl => list_rev_aux_fwd T tl (list_t.ListCons hd lo)
-    | list_t.ListNil => Result.ret lo
+    | list_t.Cons hd tl => list_rev_aux_fwd T tl (list_t.Cons hd lo)
+    | list_t.Nil => Result.ret lo
   
   /- [no_nested_borrows::list_rev] -/
   def list_rev_fwd_back (T : Type) (l : list_t T) : Result (list_t T) :=
-    let li := mem_replace_fwd (list_t T) l list_t.ListNil
-    list_rev_aux_fwd T li list_t.ListNil
+    let li := mem_replace_fwd (list_t T) l list_t.Nil
+    list_rev_aux_fwd T li list_t.Nil
   
   /- [no_nested_borrows::test_list_functions] -/
   def test_list_functions_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
-      let l0 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l
-      let l1 := list_t.ListCons (Int32.ofNatCore 1 (by intlit)) l0
+      let l := list_t.Nil
+      let l0 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l
+      let l1 := list_t.Cons (Int32.ofNatCore 1 (by intlit)) l0
       let i ←
-        list_length_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit))
-          l1)
+        list_length_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1)
       if h: not (i = (UInt32.ofNatCore 3 (by intlit)))
       then Result.fail Error.panic
       else
         do
           let i0 ←
-            list_nth_shared_fwd Int32 (list_t.ListCons
+            list_nth_shared_fwd Int32 (list_t.Cons
               (Int32.ofNatCore 0 (by intlit)) l1)
               (UInt32.ofNatCore 0 (by intlit))
           if h: not (i0 = (Int32.ofNatCore 0 (by intlit)))
@@ -356,7 +354,7 @@ structure OpaqueDefs where
           else
             do
               let i1 ←
-                list_nth_shared_fwd Int32 (list_t.ListCons
+                list_nth_shared_fwd Int32 (list_t.Cons
                   (Int32.ofNatCore 0 (by intlit)) l1)
                   (UInt32.ofNatCore 1 (by intlit))
               if h: not (i1 = (Int32.ofNatCore 1 (by intlit)))
@@ -364,7 +362,7 @@ structure OpaqueDefs where
               else
                 do
                   let i2 ←
-                    list_nth_shared_fwd Int32 (list_t.ListCons
+                    list_nth_shared_fwd Int32 (list_t.Cons
                       (Int32.ofNatCore 0 (by intlit)) l1)
                       (UInt32.ofNatCore 2 (by intlit))
                   if h: not (i2 = (Int32.ofNatCore 2 (by intlit)))
@@ -372,7 +370,7 @@ structure OpaqueDefs where
                   else
                     do
                       let ls ←
-                        list_nth_mut_back Int32 (list_t.ListCons
+                        list_nth_mut_back Int32 (list_t.Cons
                           (Int32.ofNatCore 0 (by intlit)) l1)
                           (UInt32.ofNatCore 1 (by intlit))
                           (Int32.ofNatCore 3 (by intlit))
@@ -550,8 +548,8 @@ structure OpaqueDefs where
   /- [no_nested_borrows::test_shared_borrow_enum1] -/
   def test_shared_borrow_enum1_fwd (l : list_t UInt32) : Result UInt32 :=
     match h: l with
-    | list_t.ListCons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit))
-    | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit))
+    | list_t.Cons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit))
+    | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit))
   
   /- [no_nested_borrows::test_shared_borrow_enum2] -/
   def test_shared_borrow_enum2_fwd : Result UInt32 :=
diff --git a/tests/lean/misc-paper/Paper.lean b/tests/lean/misc-paper/Paper.lean
index 4faf36ee..05fde52c 100644
--- a/tests/lean/misc-paper/Paper.lean
+++ b/tests/lean/misc-paper/Paper.lean
@@ -58,57 +58,56 @@ structure OpaqueDefs where
   
   /- [paper::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
   
   /- [paper::list_nth_mut] -/
   def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [paper::list_nth_mut] -/
   def list_nth_mut_back
     (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl)
+      then Result.ret (list_t.Cons ret0 tl)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl0 ← list_nth_mut_back T tl i0 ret0
-          Result.ret (list_t.ListCons x tl0)
-    | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x tl0)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [paper::sum] -/
   def sum_fwd (l : list_t Int32) : Result Int32 :=
     match h: l with
-    | list_t.ListCons x tl => do
-                                let i ← sum_fwd tl
-                                Int32.checked_add x i
-    | list_t.ListNil => Result.ret (Int32.ofNatCore 0 (by intlit))
+    | list_t.Cons x tl => do
+                            let i ← sum_fwd tl
+                            Int32.checked_add x i
+    | list_t.Nil => Result.ret (Int32.ofNatCore 0 (by intlit))
   
   /- [paper::test_nth] -/
   def test_nth_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
-      let l0 := list_t.ListCons (Int32.ofNatCore 3 (by intlit)) l
-      let l1 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l0
+      let l := list_t.Nil
+      let l0 := list_t.Cons (Int32.ofNatCore 3 (by intlit)) l
+      let l1 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l0
       let x ←
-        list_nth_mut_fwd Int32 (list_t.ListCons (Int32.ofNatCore 1 (by intlit))
-          l1) (UInt32.ofNatCore 2 (by intlit))
+        list_nth_mut_fwd Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) l1)
+          (UInt32.ofNatCore 2 (by intlit))
       let x0 ← Int32.checked_add x (Int32.ofNatCore 1 (by intlit))
       let l2 ←
-        list_nth_mut_back Int32 (list_t.ListCons
-          (Int32.ofNatCore 1 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit))
-          x0
+        list_nth_mut_back Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit))
+          l1) (UInt32.ofNatCore 2 (by intlit)) x0
       let i ← sum_fwd l2
       if h: not (i = (Int32.ofNatCore 7 (by intlit)))
       then Result.fail Error.panic
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