sara lee (Aug 08 2021 at 14:05): 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?
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.
sara lee (Aug 10 2021 at 17:22):(deleted)
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