coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?

From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
To: coq club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?
Date: Sun, 13 Apr 2014 06:21:25 +0300

Thanks for your answer, it worked! I don't understand how can this
code work, though. Because pattern matching has different return type
than the function.

Also, I tried replacing `v'` with `_` and using `refine` tactic, but I
didn't get `Vector h' 0 someFreshVar = v'` as hypothesis while filling
the case with `as v'`. Why I never get this types of equalities in
pattern matching?

Thanks again.

---
Ömer Sinan Ağacan
http://osa1.net

[Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, Ömer Sinan Ağacan, 04/12/2014
- Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, Arthur Azevedo de Amorim, 04/12/2014
  - Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, Ömer Sinan Ağacan, 04/13/2014
    - Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, Abhishek Anand, 04/13/2014
    - Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, AUGER Cédric, 04/13/2014
    - Re: [Coq-Club] Pattern matching on vectors: How to tell Coq that tail is one shorter than the discriminee?, Arthur Azevedo de Amorim, 04/14/2014