I'm new to Coq and I'm on my own (self-learning).
Define a function list_min that takes a list of natural numbers and returns the least element of the list.
Fixpoint list_min (l : list nat) : option nat := match l with | nil => None | cons h nil => Some h | cons h (cons h' t') => list_min (cons (min h h') t') end.
Error: Recursive definition of list_min is ill-formed. In environment list_min : list nat -> option nat l : list nat h : nat l0 : list nat h' : nat t' : list nat Recursive call to list_min has principal argument equal to "cons (min h h') t'" instead of one of the following variables: "l0" "t'". Recursive definition is: "fun l : list nat => match l with | nil => None | cons h nil => Some h | cons h (cons h' t') => list_min (cons (min h h') t') end".
- Where does
- Is there a way to inform Coq such that
(cons x y)is shorter than
(cons (cons x y))and thus my
list_natwill always terminate?