diff options
Diffstat (limited to 'tests/lean/misc-loops')
| -rw-r--r-- | tests/lean/misc-loops/Loops/Funs.lean | 200 | ||||
| -rw-r--r-- | tests/lean/misc-loops/Loops/Types.lean | 4 |
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 |