The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Dear Coq users,

I admit being one of those victims of dependent types, though Adam's
book is a benediction for newbies.

I am currently facing a somewhat simple problem which is very close to
one example that can be found in Adam's book :

Lemma tricky : forall (A : Type) (X : A) (pf : A = A), X = match pf in
(_ = A) return A with refl_equal => X end.

vs.

Example example : forall (A : Type) (X : A) (pf : X = X), X = match pf
with refl_equal => X end.

Contrary to the example, the equality proof is a about the type of the
element, and not on the element itself. And I can't manage to adapt the
proof for the example, but I imagine it shall be simple (some fiddling
with the return type, i assume).

Any clues (axiom-free, of course) ?

Thanks in advance,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature