Quelle bug_16771.v Sprache: Coq

Require Import CRelationClasses.

Structure ConstructiveReals : Type :=
  {
    CRcarrier : Prop;
    CRle (x y : CRcarrier) := False;
  }.

#[local] Hint Resolve iff_equivalence : mydb.

Goal forall {R : ConstructiveReals},
    CRelationClasses.Equivalence (CRle R).
Proof.
intros.
auto with mydb.
(* Anomaly "in Univ.repr: Universe Top.169 undefined."
Please report at http://coq.inria.fr/bugs/.*)
Abort.

quality99%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.