The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

> How about a guideline that authors should use Type wherever possible
> instead of restricting themselves to Set?  (With an obvious exception for
> declaring the universe of an inductive type with no input types.)

This certainly makes sense.

> Also, I've found that as a practical matter, it's more difficult to use "if 
> and
> only if" results than the equivalent pair of split results, because "apply 
> ->"
> and "apply <-" aren't as good at unification as the stock "apply" (in
> particular they don't accept "with" specifiers).  Is this something that 
> should
> be mentioned in the guidelines, to split up "if and only if" results?

I wonder if this is best fixed by improving apply -> and apply <-
rather than working around them in the library.

  Tom