Skip to Content.
Sympa Menu

coq-club - 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?

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



Archive powered by MHonArc 2.6.18.

Top of Page