gistfile1.coq

Inductive Foo (X : Type) :      Type -> Prop :=
(*                 ^ Parameter  ^ Index *)
| Foo0 : Foo X nat.

Check Foo.


Inductive T0 : Type -> Type -> Prop :=
(*             ^       ^   Index *)
| D0 : T0 nat nat.
(* | D0 : forall (X:Type), T0 X X. *)

Inductive T1 (X : Type) : Type -> Prop :=
(*                        ^ Index *)
| D1  : T1 X nat.
(* | D1 : T1 X X. *)
(* | D1 : T1 nat nat. *)

Inductive T2 (X Y: Type) : Prop :=
| D2 : T2 X Y.

Check T0.
Check T1.
Check T2.

Check T0_ind.
(*
T0_ind
     : forall P : Type -> Type -> Prop,
       P nat nat ->
       forall T T1 : Type, T0 T T1 -> P T T1

T0_ind
     : forall P : Type -> Type -> Prop,
       (forall X : Type, P X X) ->
       forall T T1 : Type, T0 T T1 -> P T T1

 *)

Check T1_ind.
(*
T1_ind
     : forall (X : Type) (P : Type -> Prop),
       P nat -> forall T : Type, T1 X T -> P T
  *)
Check T2_ind.
(*
T2_ind
     : forall (X Y : Type) (P : Prop), P -> T2 X Y -> P
 *)