|
From Coq Require Import Bool ssreflect.
Set Printing All.
Set Debug Ssreflect.
Class Class := { sort : Type ; op : sort -> bool }.
Coercion sort : Class >-> Sortclass.
Arguments op [_] _.
Lemma opP (A: Class) (a: A) : reflect True (op a).
Proof. Admitted.
Section Section.
Context (A B: Class) (a: A).
Goal is_true (op a).
by case: opP.
Abort.
End Section.
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
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.
|
