diff options
Diffstat (limited to 'tests/lean/misc/loops')
-rw-r--r-- | tests/lean/misc/loops/Loops/Funs.lean | 70 |
1 files changed, 27 insertions, 43 deletions
diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean index 5fe5b4ff..33a3a881 100644 --- a/tests/lean/misc/loops/Loops/Funs.lean +++ b/tests/lean/misc/loops/Loops/Funs.lean @@ -32,8 +32,7 @@ def sum_with_mut_borrows_loop_fwd sum_with_mut_borrows_loop_fwd max mi0 ms0 else UInt32.checked_mul ms (UInt32.ofNatCore 2 (by intlit)) termination_by sum_with_mut_borrows_loop_fwd max mi ms => - sum_with_mut_borrows_loop_terminates - max mi ms + sum_with_mut_borrows_loop_terminates max mi ms decreasing_by sum_with_mut_borrows_loop_decreases max mi ms /- [loops::sum_with_mut_borrows] -/ @@ -52,8 +51,7 @@ def sum_with_shared_borrows_loop_fwd sum_with_shared_borrows_loop_fwd max i0 s0 else UInt32.checked_mul s (UInt32.ofNatCore 2 (by intlit)) termination_by sum_with_shared_borrows_loop_fwd max i s => - sum_with_shared_borrows_loop_terminates - max i s + sum_with_shared_borrows_loop_terminates max i s decreasing_by sum_with_shared_borrows_loop_decreases max i s /- [loops::sum_with_shared_borrows] -/ @@ -106,8 +104,7 @@ def list_nth_mut_loop_loop_fwd | list_t.ListNil => result.fail error.panic termination_by list_nth_mut_loop_loop_fwd ls i => - list_nth_mut_loop_loop_terminates - T ls i + list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i /- [loops::list_nth_mut_loop] -/ @@ -129,8 +126,7 @@ def list_nth_mut_loop_loop_back | list_t.ListNil => result.fail error.panic termination_by list_nth_mut_loop_loop_back ls i ret0 => - list_nth_mut_loop_loop_terminates - T ls i + list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i /- [loops::list_nth_mut_loop] -/ @@ -152,8 +148,7 @@ def list_nth_shared_loop_loop_fwd | list_t.ListNil => result.fail error.panic termination_by list_nth_shared_loop_loop_fwd ls i => - list_nth_shared_loop_loop_terminates - T ls i + list_nth_shared_loop_loop_terminates T ls i decreasing_by list_nth_shared_loop_loop_decreases ls i /- [loops::list_nth_shared_loop] -/ @@ -191,8 +186,8 @@ def get_elem_mut_loop_back result.ret (list_t.ListCons y tl0) | list_t.ListNil => result.fail error.panic -termination_by get_elem_mut_loop_back x ls ret0 => get_elem_mut_loop_terminates - x ls +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 /- [loops::get_elem_mut] -/ @@ -214,8 +209,8 @@ def get_elem_shared_loop_fwd if y = x then result.ret y else get_elem_shared_loop_fwd x tl | list_t.ListNil => result.fail error.panic -termination_by get_elem_shared_loop_fwd x ls => get_elem_shared_loop_terminates - x ls +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 /- [loops::get_elem_shared] -/ @@ -251,8 +246,7 @@ def list_nth_mut_loop_with_id_loop_fwd | list_t.ListNil => 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 + list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls /- [loops::list_nth_mut_loop_with_id] -/ @@ -277,8 +271,7 @@ def list_nth_mut_loop_with_id_loop_back | list_t.ListNil => 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 + list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls /- [loops::list_nth_mut_loop_with_id] -/ @@ -303,8 +296,7 @@ def list_nth_shared_loop_with_id_loop_fwd | list_t.ListNil => 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 + list_nth_shared_loop_with_id_loop_terminates T i ls decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls /- [loops::list_nth_shared_loop_with_id] -/ @@ -334,8 +326,7 @@ def list_nth_mut_loop_pair_loop_fwd | list_t.ListNil => 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 + list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i /- [loops::list_nth_mut_loop_pair] -/ @@ -366,8 +357,7 @@ def list_nth_mut_loop_pair_loop_back'a | list_t.ListNil => 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 + list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i /- [loops::list_nth_mut_loop_pair] -/ @@ -398,8 +388,7 @@ def list_nth_mut_loop_pair_loop_back'b | list_t.ListNil => 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 + list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i /- [loops::list_nth_mut_loop_pair] -/ @@ -429,8 +418,7 @@ def list_nth_shared_loop_pair_loop_fwd | list_t.ListNil => 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 + list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i /- [loops::list_nth_shared_loop_pair] -/ @@ -460,8 +448,7 @@ def list_nth_mut_loop_pair_merge_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_loop_pair_merge] -/ @@ -495,7 +482,7 @@ def list_nth_mut_loop_pair_merge_loop_back | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_loop_pair_merge] -/ @@ -525,8 +512,7 @@ def list_nth_shared_loop_pair_merge_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_shared_loop_pair_merge] -/ @@ -556,8 +542,7 @@ def list_nth_mut_shared_loop_pair_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_shared_loop_pair] -/ @@ -588,7 +573,7 @@ def list_nth_mut_shared_loop_pair_loop_back | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_shared_loop_pair] -/ @@ -618,7 +603,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_shared_loop_pair_merge] -/ @@ -650,7 +635,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_back | list_t.ListNil => 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 + 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 /- [loops::list_nth_mut_shared_loop_pair_merge] -/ @@ -680,8 +665,7 @@ def list_nth_shared_mut_loop_pair_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_shared_mut_loop_pair] -/ @@ -712,7 +696,7 @@ def list_nth_shared_mut_loop_pair_loop_back | list_t.ListNil => 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 + 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 /- [loops::list_nth_shared_mut_loop_pair] -/ @@ -742,7 +726,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd | list_t.ListNil => 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 + 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 /- [loops::list_nth_shared_mut_loop_pair_merge] -/ @@ -774,7 +758,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_back | list_t.ListNil => 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 + 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 /- [loops::list_nth_shared_mut_loop_pair_merge] -/ |