coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrew Polonsky <andrew.polonsky AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] what does this error message mean?
- Date: Wed, 13 Mar 2013 16:12:26 -0400
Definition obs (Phi: Type -> Type -> Type) {A:Type} (a a': A) : Type :=
forall P : A -> Type, Phi (P a) (P a').
CoInductive eq (A B: Type) : Type :=
| cons (f:A->B) (g:B->A)
(eta: forall (a:A) (b:B),
(eq (obs eq a (g b)) (obs eq b (f a)))
* (eq (obs eq b (f a)) (obs eq (g b) a)))
: eq A B.
Anomaly: Trying to substitute an algebraic universe where only levels are allowed.
Please report.
forall P : A -> Type, Phi (P a) (P a').
CoInductive eq (A B: Type) : Type :=
| cons (f:A->B) (g:B->A)
(eta: forall (a:A) (b:B),
(eq (obs eq a (g b)) (obs eq b (f a)))
* (eq (obs eq b (f a)) (obs eq (g b) a)))
: eq A B.
Anomaly: Trying to substitute an algebraic universe where only levels are allowed.
Please report.
- [Coq-Club] what does this error message mean?, Andrew Polonsky, 03/13/2013
- Re: [Coq-Club] what does this error message mean?, Hugo Herbelin, 03/14/2013
Archive powered by MHonArc 2.6.18.