Pavel Shuhray (May 18 2024 at 17:35): Pavel Shuhray (May 18 2024 at 17:35):How to do it right?
Inductive A : forall (n:nat), Set :=
| foo : forall (n:nat), A n -> A (S n).
Fixpoint iterate (n:nat) (m:nat) (a : A m): A (n + m) :=
match n with
| 0 => a
| S n => foo (n + m) (iterate n a)
end.
@Pavel Shuhray you forgot m in iterate
Fixpoint iterate (n:nat) (m:nat) (a : A m): A (n + m) :=
match n with
| 0 => a
| S n => foo (n + m) (iterate n m a)
end.
Thomas Lamiaux said:
Pavel Shuhray you forgot m in iterate
Thank you:)
Last updated: Oct 13 2024 at 01:02 UTC