| /-! | |
| More tests related to structural indices depending on fixed parameters | |
| -/ | |
| inductive T (n : Nat) : Nat → Type where | |
| | zero : T n 0 | |
| | succ {i} : T n i → T n (i + n) → T n i | |
| /-- | |
| error: cannot use specified measure for structural recursion: | |
| its type is an inductive datatype | |
| T (↑f) i | |
| and the datatype parameter | |
| ↑f | |
| depends on the function parameter | |
| i | |
| which is not fixed. | |
| -/ | |
| #guard_msgs in | |
| def foo (i : Nat) (f : Fin i) : T f i → Unit | |
| | .zero => () | |
| | .succ t _ => foo i f t | |
| termination_by structural t => t | |
| def bar (a : Nat) (i : Nat) (f : Fin a) : T f i → Unit | |
| | .zero => () | |
| | .succ t _ => bar a i f t | |
| termination_by structural t => t | |
| /-- | |
| info: bar.induct (a : Nat) (f : Fin a) (motive : (i : Nat) → T (↑f) i → Prop) (case1 : motive 0 T.zero) | |
| (case2 : ∀ (i : Nat) (t : T (↑f) i) (a_1 : T (↑f) (i + ↑f)), motive i t → motive i (t.succ a_1)) (i : Nat) | |
| (a✝ : T (↑f) i) : motive i a✝ | |
| -/ | |
| #guard_msgs in | |
| #check bar.induct |