coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] About Inductive parameters in the Reference Manual

From: <lars.rasmusson AT sics.se>
To: coq-club AT inria.fr
Subject: [Coq-Club] About Inductive parameters in the Reference Manual
Date: Fri, 14 Nov 2014 17:49:54 +0100

On page 120 of the Reference Manual
https://coq.inria.fr/distrib/V8.4pl3/files/Reference-Manual.pdf

here (see http://oi61.tinypic.com/11juk41.jpg for a extract from the page)
it says

C == forall p_1...p_r, forall a_1...a_n, (I p1 ... p_r t_1 ... t_q)

Should it be the following?

C == forall p_1...p_r, forall a_1...a_n, (I p1 ... p_r a_1 ... a_n)

Best regards,
/Lars

[Coq-Club] About Inductive parameters in the Reference Manual, lars.rasmusson, 11/14/2014
- Re: [Coq-Club] About Inductive parameters in the Reference Manual, Ali Assaf, 11/14/2014