Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Perm.thy
Sprache: Coq
|
From Coq Require Import Utf8 Bool ssreflect.
Set Printing All.
Set Debug Ssreflect.
Class Class sort := { op : sort → bool }.
Arguments op {_ _}.
Hint Mode Class !.
Lemma opP A (C: Class A) (a: A) : reflect True (op a).
Proof. Admitted.
Arguments op {_ _}.
Section Section.
Context A B (CA : Class A) (CB : Class B) (a: A).
Goal is_true (op a).
by case: opP.
Abort.
End Section.
[ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
]
|
|
