The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Is there any way accessible via Ltac that one can get the count of the 
number of indexes for a particular inductive type?  Not the total number 
of parameters - just the indexes.

Examining the inductive type doesn't tell you which of that type's args 
are indexes or just parameters.

Examining the constructors usually helps some, because the point where 
the args of the constructors differ from each other or the args of the 
type indicates that there are no more non-indexes after that point.  
But, there may be indexes that don't vary. Hence, in:

Inductive Foo : nat -> Set := foo(n : nat) : Foo n.

Inductive Bar(n : nat) : Set := bar.

Foo and Bar have the same type nat -> Set, and their constructors foo 
and bar have similar type structure as well (modulo Foo/Bar).  Yet, Foo 
has a type index while Bar doesn't.

-- Jonathan