coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dependent Type Minimal Example

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Dependent Type Minimal Example
Date: Sun, 18 Aug 2013 16:09:41 +0000

Hi,

Can someone post a minimal solution to this (without using dep_destruct from cpdt tactics) ?

https://gist.github.com/anonymous/6262395

Proofs involving dependent types seems to high levels of "black magic" which makes it nearly impossible to debug. I'd like to see a minimal "manual" solution to see what's going on.

Thanks

[Coq-Club] Dependent Type Minimal Example, t x, 08/18/2013
- [Coq-Club] Re: Dependent Type Minimal Example, t x, 08/18/2013
  - Re: [Coq-Club] Re: Dependent Type Minimal Example, Hugo Carvalho, 08/18/2013
    - Re: [Coq-Club] Re: Dependent Type Minimal Example, t x, 08/19/2013
- Re: [Coq-Club] Dependent Type Minimal Example, Matthieu Sozeau, 08/20/2013