Quelle bug_5243.v Sprache: Coq

Typeclasses eauto := debug.

Class Foo A := foo : A.

Hint Extern 0 (Foo _) => lazy beta delta; give_up : typeclass_instances.

Lemma t A : A.
  notypeclasses refine ((_ : Foo A)).
  typeclasses eauto.

(*
No more subgoals, but there are some goals you gave up:

A

You need to go back and solve them.
*)

Abort.

Lemma t A : A.
  refine ((_ : Foo A)).

(*
1: looking for (Foo A) without backtracking
1.1: (*external*)
(Foo A), 0 subgoal(s)
leaking evar 10
A

Anomaly:
File "tactics/class_tactics.ml", line 1345, characters 11-17: Assertion failed.
Please report at http://coq.inria.fr/bugs/.
*)
  Unshelve.
  all:fail. (* no more goals *)
  Fail Qed.
Abort.

quality99%

¤ Dauer der Verarbeitung: 0.4 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.