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?
It depends how you write the fact that an element belongs to the list. The idea would be to use
n:=list_max l. This gives you a
Forall statement that you can turn into an
In statement by using
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