The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here is a way to distinguish based on the results of typechecking:

Inductive eq : forall {A}, A -> A -> Prop := eq_refl A x : @eq A x x.

Inductive eq' {A} (x : A) : A -> Prop := eq_refl' : @eq' A x x.

Check fun A x y (p : @eq A x y) => match p in (@eq A' x' y') with _ => I end.

Fail Check fun A x y (p : @eq' A x y) => match p in (@eq' A' x' y') with _ => I end. (* Error: The parameters do not bind in patterns; they must be replaced by '_'. *)

I wish you luck in making this work in general; it seems that the [in] clause does special name-resolution and ignores ltac-variables.

Here's another way that may prove more fruitful:

Goal forall A x y, @eq A x y -> True.

  intros ??? p.

  case p. (* forall A0 : Type, A0 -> True *)

Abort.

Goal forall A x y, @eq' A x y -> True.

  intros ??? p.

  case p. (* True *)

Abort.

On Wed, Jul 20, 2016 at 1:25 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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