The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT students.cs.unibo.it>]

Hi,

I need something like this:

Inductive equal1 : (A:Type)(B:Type) A -> B -> Prop :=
 eq1 : (A:Type)(B:Type)(a:A)(b:B)(A==B)->(a==b)->(equal1 A B a b).

But this fails to typecheck, because a and b are of different types.
But if (A==B) then I expect (a == b) to typecheck (perhaps B should
be automatically coerced to A).

If I define an inductive type as

Inductive T : Type := c : (A:Type) A -> T.

then this is another way of defining equal1:

Definition equal1 := [A:Type][B:Type][a:A][b:B](c A a)==(c B b).

But if I try:

Goal (eq1 nat nat O (S O))->False.
 Intros ; Unfold eq1 in H ; Discriminate.

I get

Uncaught exception: File "equality.ml", line 0, characters 20213-20225:
Assertion failed
If this is in user-written tactic code, then it needs to be modified.
If this is in system code, then
it needs to be reported.

This happens either with

Welcome to Coq V6.3 (July 1999)

and with V6.2.

Is it possible to do it? How?

                                                T.I.A.
                                                C.S.C.
-- 
-----------------------------------------
Real Name: Claudio Sacerdoti Coen
Address: via del Colle n.6
         S. Lazzaro di Savena (BO)
         Italy
e-mail:  
sacerdot AT cs.unibo.it
-----------------------------------------