coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why this does not compile?

From: Victor Porton <porton AT narod.ru>
To: Coq <coq-club AT inria.fr>
Subject: [Coq-Club] Why this does not compile?
Date: Sun, 06 Nov 2011 06:22:04 +0400
Envelope-from: porton AT yandex.ru

Why this does not compile?

[[[
Class Relation {set: Set} := {
}.

Definition compose_relation_classes {set:Set} (f g: @Relation set) :=
Build_Relation.

Definition my_trans2(r: Relation) := compose_relation_classes r r = r.
]]]

--
Victor Porton - http://portonvictor.org

[Coq-Club] Why this does not compile?, Victor Porton
- Re: [Coq-Club] Why this does not compile?, Pierre Casteran