The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello Everyone

I have an indexed class of types (F) and I would like to define a
coercion that is only defined on a part of this class (F 0).

Is this at all possible?

This is what I have tried so far:
-------------------------Coq -----------------------------

Variable F : nat -> Type.
Variable A : F 0.

SubClass F0 := F 0.

Inductive C := 
  C1 : bool -> C 
| C2 : F 0 -> C.

(* Coercion C2 : F >-> C. *)
(* Error: C2 does not respect the inheritance uniform condition. *)

(* Coercion C2 : F0 >-> C. *)
(* Error: Cannot recognize F0 as a source class of C2. *)

(* The closest I get is this: *)

Inductive C' := 
  C1' : bool -> C' 
| C2' : F0 -> C'.

Coercion C2' : F0 >-> C'.

------------------------------------------------------------

Is there any way to define something that would behave like 
a coercion from F 0 to F0?

Coercion ??? F 0 >-> F0


Ideally [ C1' true ; A ] would be accepted.

-- 
Regards
Christian