The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks for your patience. My previous notation is terrible and I have changed it a bit.

I believe https://gist.github.com/anonymous/7112657 fixes both issues on line 22.

Is there anything still wrong with this?

Thanks!

On Tue, Oct 22, 2013 at 7:55 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 10/22/2013 09:57 AM, t x wrote:

Is https://gist.github.com/anonymous/7100956 correct?
Where error (1) is fixed at line 18 and error (2) is fixed at line 21.

No, there are still issues.
- You can't just write "typeof(Di)"; it's necessary to extend the typing context with variables "y*_*" of appropriate types.
- On the same line, you substitute "u_i" for "x_i", which can't be right, because "u_i" is independent of which pattern has matched.  You need to use the type of "Cn" to figure out the right terms to substitute.