The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

On 2016-09-09 09:26, "Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 writes:

> Dear Alan,
>
> since I have quite some issues with proof irrelevance of equalities, I
> find this quite interesting.
>
> One thing I don't understand: Is "nu_canon" supposed to hold for all "nu" or
> just for some specific "nu"? Declaring "nu" as Variable makes me believe the
> first, but in eqdec_canon you use a specific nu (nudec), so it is not clear 
> to
> me in how far the conclusion of eqdec_canon is equivalent to nu_canon.

nu_cannon is supposed to hold for the given nu. It would probably be
better expressed as a dependent record.

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-08: 398.93, 2016-08: 402.25

Attachment: signature.asc
Description: PGP signature