diff options
| -rw-r--r-- | compiler/Extract.ml | 10 | ||||
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 34 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 32 | ||||
| -rw-r--r-- | tests/lean/misc/loops/Loops/Funs.lean | 70 |
4 files changed, 60 insertions, 86 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1057cc3b..a995ee7f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2379,9 +2379,11 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_terminates_clause def.def_id def.loop_id ctx in F.pp_print_break fmt 0 0; + (* Open a box for the whole {terminates_by CALL => DECREASES } *) + F.pp_open_hvbox fmt ctx.indent_incr; + (* Open a box for {terminates_by CALL =>} *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "termination_by"; - F.pp_open_hovbox fmt 0; F.pp_print_space fmt (); F.pp_print_string fmt def_name; List.iter @@ -2391,9 +2393,11 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) all_vars; F.pp_print_space fmt (); F.pp_print_string fmt "=>"; + (* Close the box for {terminates_by CALL =>} *) F.pp_close_box fmt (); - F.pp_open_hovbox fmt 0; F.pp_print_space fmt (); + (* Open the box for {DECREASES} *) + F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt terminates_name; List.iter (fun (p : type_var) -> @@ -2406,7 +2410,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt (ctx_get_var v ctx_body)) vars; + (* Close the box for {DECREASES} *) F.pp_close_box fmt (); + (* Close the box for the whole {terminates_by CALL => DECREASES } *) F.pp_close_box fmt (); let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 030b335a..1b03b7a2 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -20,8 +20,7 @@ def hash_map_allocate_slots_loop_fwd hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hash_map_allocate_slots_loop_fwd slots n => - hash_map_allocate_slots_loop_terminates - T slots n + hash_map_allocate_slots_loop_terminates T slots n decreasing_by hash_map_allocate_slots_loop_decreases slots n /- [hashmap::HashMap::{0}::allocate_slots] -/ @@ -67,8 +66,7 @@ def hash_map_clear_loop_fwd_back hash_map_clear_loop_fwd_back T slots0 i1 else result.ret slots termination_by hash_map_clear_loop_fwd_back slots i => - hash_map_clear_loop_terminates - T slots i + hash_map_clear_loop_terminates T slots i decreasing_by hash_map_clear_loop_decreases slots i /- [hashmap::HashMap::{0}::clear] -/ @@ -101,8 +99,7 @@ def hash_map_insert_in_list_loop_fwd | list_t.ListNil => result.ret true termination_by hash_map_insert_in_list_loop_fwd key value ls => - hash_map_insert_in_list_loop_terminates - T key value ls + hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ @@ -125,8 +122,7 @@ def hash_map_insert_in_list_loop_back let l := list_t.ListNil result.ret (list_t.ListCons key value l) termination_by hash_map_insert_in_list_loop_back key value ls => - hash_map_insert_in_list_loop_terminates - T key value ls + hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ @@ -189,7 +185,7 @@ def hash_map_move_elements_from_list_loop_fwd_back | list_t.ListNil => result.ret ntable termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls => - hash_map_move_elements_from_list_loop_terminates T ntable ls + hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -215,7 +211,7 @@ def hash_map_move_elements_loop_fwd_back hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) termination_by hash_map_move_elements_loop_fwd_back ntable slots i => - hash_map_move_elements_loop_terminates T ntable slots i + hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hash_map_move_elements_loop_decreases ntable slots i /- [hashmap::HashMap::{0}::move_elements] -/ @@ -281,8 +277,7 @@ def hash_map_contains_key_in_list_loop_fwd | list_t.ListNil => result.ret false termination_by hash_map_contains_key_in_list_loop_fwd key ls => - hash_map_contains_key_in_list_loop_terminates - T key ls + hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hash_map_contains_key_in_list_loop_decreases key ls /- [hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -311,8 +306,7 @@ def hash_map_get_in_list_loop_fwd | list_t.ListNil => result.fail error.panic termination_by hash_map_get_in_list_loop_fwd key ls => - hash_map_get_in_list_loop_terminates - T key ls + hash_map_get_in_list_loop_terminates T key ls decreasing_by hash_map_get_in_list_loop_decreases key ls /- [hashmap::HashMap::{0}::get_in_list] -/ @@ -341,8 +335,7 @@ def hash_map_get_mut_in_list_loop_fwd | list_t.ListNil => result.fail error.panic termination_by hash_map_get_mut_in_list_loop_fwd ls key => - hash_map_get_mut_in_list_loop_terminates - T ls key + hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -364,8 +357,7 @@ def hash_map_get_mut_in_list_loop_back | list_t.ListNil => result.fail error.panic termination_by hash_map_get_mut_in_list_loop_back ls key ret0 => - hash_map_get_mut_in_list_loop_terminates - T ls key + hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -420,8 +412,7 @@ def hash_map_remove_from_list_loop_fwd | list_t.ListNil => result.ret Option.none termination_by hash_map_remove_from_list_loop_fwd key ls => - hash_map_remove_from_list_loop_terminates - T key ls + hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ @@ -449,8 +440,7 @@ def hash_map_remove_from_list_loop_back | list_t.ListNil => result.ret list_t.ListNil termination_by hash_map_remove_from_list_loop_back key ls => - hash_map_remove_from_list_loop_terminates - T key ls + hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5134f483..2795ecfa 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -24,8 +24,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => - hashmap_hash_map_allocate_slots_loop_terminates - T slots n + hashmap_hash_map_allocate_slots_loop_terminates T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -76,8 +75,7 @@ def hashmap_hash_map_clear_loop_fwd_back hashmap_hash_map_clear_loop_fwd_back T slots0 i1 else result.ret slots termination_by hashmap_hash_map_clear_loop_fwd_back slots i => - hashmap_hash_map_clear_loop_terminates - T slots i + hashmap_hash_map_clear_loop_terminates T slots i decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ @@ -113,7 +111,7 @@ def hashmap_hash_map_insert_in_list_loop_fwd | hashmap_list_t.HashmapListNil => result.ret true termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -139,7 +137,7 @@ def hashmap_hash_map_insert_in_list_loop_back result.ret (hashmap_list_t.HashmapListCons key value l) termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -209,8 +207,8 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back | hashmap_list_t.HashmapListNil => result.ret ntable termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls - => hashmap_hash_map_move_elements_from_list_loop_terminates T - ntable ls + => + hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -242,7 +240,7 @@ def hashmap_hash_map_move_elements_loop_fwd_back hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => - hashmap_hash_map_move_elements_loop_terminates T ntable slots i + hashmap_hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ @@ -309,7 +307,7 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd | hashmap_list_t.HashmapListNil => result.ret false termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => - hashmap_hash_map_contains_key_in_list_loop_terminates T key ls + hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -339,8 +337,7 @@ def hashmap_hash_map_get_in_list_loop_fwd | hashmap_list_t.HashmapListNil => result.fail error.panic termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => - hashmap_hash_map_get_in_list_loop_terminates - T key ls + hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -370,8 +367,7 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd | hashmap_list_t.HashmapListNil => result.fail error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => - hashmap_hash_map_get_mut_in_list_loop_terminates - T ls key + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -395,7 +391,7 @@ def hashmap_hash_map_get_mut_in_list_loop_back | hashmap_list_t.HashmapListNil => result.fail error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => - hashmap_hash_map_get_mut_in_list_loop_terminates T ls key + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -458,8 +454,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd | hashmap_list_t.HashmapListNil => result.ret Option.none termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => - hashmap_hash_map_remove_from_list_loop_terminates - T key ls + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -490,8 +485,7 @@ def hashmap_hash_map_remove_from_list_loop_back | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil termination_by hashmap_hash_map_remove_from_list_loop_back key ls => - hashmap_hash_map_remove_from_list_loop_terminates - T key ls + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ 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] -/ |