Stream: Coq users

Topic: Check on output list


view this post on Zulip zeesha huq (Feb 04 2024 at 08:25):

Fixpoint check ( n a val: nat) : list nat:=
match n with
| O => [a]
| S n' => if val <=? 8 then
a::(check n' a val)
else
(check n' a val)
end. I want to stop the iterative process when number of elements in the output list become equal to
a number (let 3). How to perform pattern matching on output list?

view this post on Zulip zeesha huq (Feb 04 2024 at 08:25):

Fixpoint check ( n a val: nat) : list nat:=
match n with
| O => [a]
| S n' => if val <=? 8 then
a::(check n' a val)
else
(check n' a val)
end.

view this post on Zulip zeesha huq (Feb 04 2024 at 08:25):

(deleted)

view this post on Zulip zeesha huq (Feb 04 2024 at 08:26):

(deleted)


Last updated: Jun 13 2024 at 21:01 UTC