Document base case of List.for_all and List.exists

[glennsl]

The base case of List.for_all is not immediately obvious to me, so I think it'd be nice to have it documented. And while the base case of List.exists is much more obvious just from its name, I documented the base case of that as well, just for consistency.

[Octachron]

I think that adding the documentation for the behavior with respect to [] is a good idea.
What do you think of a more declarative wording, something like

For any [p], `List.for_all p []` is always [true]

?

( Note that there are few generic way to remember the base case here. For instance, for a well-behaved f, both for_all f and exists f are monoid morphisms: for_all f from (list,@) to (bool, &&) (i.e. List.forall f (x @ y) = List.forall f x && List.for_all f y ) and exists f from (list,@) to (bool, ||). And (by definition) monoid morphisms map the neutral element from the source monoid to the neutral element of the target monoid. (I am of course not suggesting to add that point to the document))

[glennsl]

Thanks for the explanation! I did actually look up the mathematical definition of universal quantification in predicate logic as well, which said it was a vacuous truth, but that just seems like an axiom. Your explanation actually makes sense.

What do you think of a more declarative wording...

Absolutely. I chose the current wording to try to be consistent with other similar docstrings, for example that of nth_opt:

Return the n-th element of the given list. The first element (head of the list) is at position 0. Return None if the list is too short. Raise Invalid_argument "List.nth" if n is negative.

But just say the word, then I'll change it.

[Octachron]

You are right, your proposition is more in line in the current style, but maybe merging the two parts would work better:

That is, it returns
   [(p a1) && (p a2) && ... && (p an)] if the list is non-empty
   and [true] otherwise.

or we could swap the two:

That is, it returns [true] is the list is empty and
   [(p a1) && (p a2) && ... && (p an)] otherwise.

[glennsl]

Done, but I made it slightly more explicit:

That is, it returns [(p a1) && (p a2) && ... && (p an)]] for a non-empty list and [true] if the list is empty.

[Octachron]

It looks good to me. You may want to add a Change entry with your contribution.

[glennsl]

You may want to add a Change entry with your contribution.

Done. I figured this change was too trivial for that, but I think I got the formalities right now.

[Octachron]

Merged, thanks for the contribution!