coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] finite sets in proofs, (continued)
- Re: [Coq-Club] finite sets in proofs, Pierre Casteran
- Re: [Coq-Club] finite sets in proofs, AUGER
- RE: [Coq-Club] finite sets in proofs, Georges Gonthier
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs,
Thomas Braibant
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs, Thomas Braibant
- Re: [Coq-Club] finite sets in proofs,
Stéphane Lescuyer
- Re: [Coq-Club] finite sets in proofs, Pierre Letouzey
- Re: [Coq-Club] finite sets in proofs, Chantal Keller
- [Coq-Club] Yet another dependent type question, Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question, Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs,
Thomas Braibant
Archive powered by MhonArc 2.6.16.