Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Yet another dependent type question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Yet another dependent type question


chronological Thread 
  • From: Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Yet another dependent type question
  • Date: Fri, 26 Mar 2010 14:45:52 +0100

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




Archive powered by MhonArc 2.6.16.

Top of Page