The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Hi all.

In Coq.Logic.Eqdep_dec there is a proof (packaged in 'Module') of 
Uniqueness of Identity Proofs for any type with decidable equality. So 
I've tried to obtain a specific proof for 'nat' since 'nat' has 
decidable equality:

Require Coq.Logic.Eqdep_dec.
Require Coq.Arith.Peano_dec.
Module eq_dec_nat : Coq.Logic.Eqdep_dec.DecidableType.
   Definition U := Coq.Init.Datatypes.nat.
   Definition eq_dec := Coq.Arith.Peano_dec.eq_nat_dec.
End eq_dec_nat.
Module eq_dec_nat_facts
   := Coq.Logic.Eqdep_dec.DecidableEqDep eq_dec_nat.
Check eq_dec_nat_facts.eq_rect_eq 0.

Error: The term "0" has type "nat" while it is expected to have type
"eq_dec_nat.U".

But 'eq_dec_nat.U = Coq.Init.Datatypes.nat' by definition of eq_dec_nat…

--
Best regards,
 Roman Beslik.