The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Doing "Set Printing All" reveals what the problem is:

Toplevel input, characters 54-73:
Error: The term "@f_equal2 nat nat Prop lt x1 y1 x2 y2 eq1 eq2" has type
 "@eq Prop (lt x1 x2) (lt y1 y2)" while it is expected to have type
 "@eq Type (lt x1 x2) (lt y1 y2)".


-Andrew

On Mon, Jul 28, 2008 at 4:08 PM, see tolearn <seetolearn AT mail.ru> wrote:

Consider theorem 'prop_eq':
> Definition prop_eq := fun p q (eq1:p=q)
       => (match eq1 in _=qdep return p->qdep
       with refl_equal => fun p=>p
       end) : p->q.

Then:
> Variable (x1 x2 y1 y2:nat) (eq1:x1=y1) (eq2:x2=y2) (lt1:x1<x2).
> Check prop_eq (x1 < x2) (y1 < y2) (f_equal2 lt eq1 eq2) lt1.
gives an error message:
{{{
Error: The term "f_equal2 lt eq1 eq2" has type "(x1 < x2) = (y1 < y2)"
 while it is expected to have type "(x1 < x2) = (y1 < y2)"
}}}
The terms actually are identic. Am I missing something? I'm
using CoqIde, coqtop version 8.1pl1 (Jul. 2007), Linux.

Best regards,
Roman Beslik.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club