The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 01/02/2015 16:07, Ilmārs Cīrulis wrote:
> Look at theorem L1 and the following "Eval compute in ..." where proof
> with wrong type is accepted. (File attached.)

This is no wrong type. If you look at the definition of "<" on
positives, you see that "1 < 333" and "1 < 4" are actually the same
type. Indeed,

Eval compute in 1 < 133.
     = Lt = Lt
     : Prop

Eval compute in 1 < 4.
     = Lt = Lt
     : Prop

So that the two terms you produce must only be mere inhabitants of the
type "Lt = Lt".

PMP

Attachment: signature.asc
Description: OpenPGP digital signature