Stream: Coq users

Topic: Iteration with parameter.


view this post on Zulip 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.

view this post on Zulip Thomas Lamiaux (May 18 2024 at 18:39):

@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.

view this post on Zulip Pavel Shuhray (May 18 2024 at 18:49):

Thomas Lamiaux said:

Pavel Shuhray you forgot m in iterate

Thank you:)


Last updated: Jun 13 2024 at 19:02 UTC