The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Dear all,

I am reading the 4th chapter of COQ reference manual - "Calculus of Inductive Constructions" and have a question about "Inductive parameters" and "real arguments" in "4.5.1 Representing an inductive definition".

According to the manual, an inductive definition Ind(Γ)(ΓI:=ΓC ) admits r inductive parameters if each type of constructors (c:C) in ΓC is such that 

C≡ ∀ p1:P1,…,∀ pr:Pr,∀ a1:A1, … ∀ an:An, (I p1 … pr t1… tq)

with I one of the inductive definitions in ΓI. We say that q is the number of real arguments of the constructor c.

The following List definition has 1 parameter:

Ind()(List:Set→Set:=nil:(∀ A:Set, List A), cons : (∀ A:Set, A → List A → List A) )

But the following definition has 0 parameter:

Ind()(List:Set→Set:=nil:(∀ A:Set, List A), cons : (∀ A:Set, A → List A → List (A*A)) )

What puzzles me is why the second definition has 0 parameter (unlike the first definition), actually I do not think I understand how to represent each of their constructors in form of ≡ ∀ p1:P1,…,∀ pr:Pr,∀ a1:A1, … ∀ an:An, (I p1 … pr t1… tq) to see their "r"...

Could anyone help?

Thank you very much

Tie