The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

Thank you,

Edsko de Vries wrote:
> Such functions are valid only in special cases; in particular, it is
> possible to use a proof as argument to a function that returns an
> argument in Set if the proof is used *only* to guard termination of the
> function, but cannot otherwise influence the value returned. If you are
> working through Coq'Art, you'll get to such functions eventually:
> Sections 14.2.3 and 15.2.

Cody Roux wrote:
> This, as well as a
> certain number of possible solutions, is discussed in the Coq'Art book
> in section 14.2 (p394).

Kouskoulas, Yanni A. wrote:
> Also, this triplet is very useful for making strongly
> specified functions that return values along with certificates
> or guarantees about the data they hold. The sig type is an example,
> see p. 252; its constructor has the type ...

I have made notes to return to this rule (variant) again when I get to
those parts of the book.