summaryrefslogtreecommitdiff
path: root/tests/lean/misc-loops
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/misc-loops')
-rw-r--r--tests/lean/misc-loops/Loops/Funs.lean200
-rw-r--r--tests/lean/misc-loops/Loops/Types.lean4
2 files changed, 102 insertions, 102 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