Stream: Coq users

Topic: Natural number list

view this post on Zulip sara lee (Aug 08 2021 at 14:05):

I have started working in Coq. I want to use list_max l function and show that all elements of list are less or equal to the value found by function ( list_max l ). What steps I should take?

view this post on Zulip Olivier Laurent (Aug 08 2021 at 14:45):

It depends how you write the fact that an element belongs to the list. The idea would be to use list_max_le with n:=list_max l. This gives you a Forall statement that you can turn into an In statement by using Forall_forall.

view this post on Zulip sara lee (Aug 10 2021 at 17:22):


view this post on Zulip zohaze (Sep 16 2021 at 16:41):

I want to write a recursive function which takes n different values from user and add them in the list. I have idea about fix value input argument but not varying values.

Last updated: Oct 04 2023 at 23:01 UTC