The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

I mean by parameter the name of variable together with

its type that one puts to the left of the : in  a definition,

by example A:Type in

 

Inductive List (A:Type):Type

 

or

 

(A:Type) and (x:A) in

 

Inductive eq (A:Type)(x:A) : A->Type

 

Regards

Patricia