Quelle bug_6714.v Sprache: Coq

Set Typeclasses Unique Instances.

Class Foo (x y : bool) := {}.
Class Bar (x y : bool) := {}.
Class Bax (x : bool) := {}.

Instance bar_1 : Bar true false := {}.
Instance bar_2 : Bar true true := {}.

Instance bax_1 : Bax false := {}.

Instance foo x y : Bar x y -> Bax y -> Foo x y := {}.

Typeclasses eauto := debug.

Fail Definition bla : Foo true _ := _.

(*
Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: 1: looking for (Foo true ?y) with backtracking
Debug: 1.1: simple apply foo on (Foo true ?y), 2 subgoal(s)
Debug: 1.1-1 : (Bar true ?y)
Debug: 1.1-1: looking for (Bar true ?y) with backtracking
Debug: 1.1-1.1: exact bar_2 on (Bar true ?y), 0 subgoal(s)
Debug: 1.1-2 : (Bax true)
Debug: 1.1-2: looking for (Bax true) without backtracking
Debug: 1.1-2: no match for (Bax true), 0 possibilities
Debug: 1.1-1.2: exact bar_1 on (Bar true ?y), 0 subgoal(s)
Debug: 1.1-2 : (Bax false)
Debug: 1.1-2: looking for (Bax false) without backtracking
Debug: 1.1-2.1: exact bax_1 on (Bax false), 0 subgoal(s)

produces bla =
foo true false bar_1 bax_1 : Foo true false
: Foo true false
*)

quality98%

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