coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
Chronological Thread
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Eduardo León <abc.deaf.xyz AT gmail.com>
- Cc: Adam Chlipala <adamc AT csail.mit.edu>, Kristopher Micinski <krismicinski AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
- Date: Sat, 29 Dec 2012 22:38:02 +0100
In Coq, pattern matching (in fact elimination of inductive types) is a
primitive concept, and the equality type is a derived concept, defined
as an inductive datatype. Pattern matching do not generate equalities,
it's the other way around: to use an equality witness, you must
pattern match on it. For further details, see the chapter of Adam's
book.
On Sat, Dec 29, 2012 at 9:56 PM, Eduardo León
<abc.deaf.xyz AT gmail.com>
wrote:
> e head of a length-indexed list guaranteed to contain at least one element?
> I understand why the auxiliary function trick works, but it looks to me like
> a hack, in the sense that `hd' Nil` has no obvious interpretation - it
> solely exists for the purpose of
- [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, abc.deaf.xyz, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Adam Chlipala, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Eduardo León, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Gabriel Scherer, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Eduardo León, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Kristopher Micinski, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Matthieu Sozeau, 12/30/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Adam Chlipala, 12/29/2012
Archive powered by MHonArc 2.6.18.