|
Axiom P : nat -> Prop.
Class class (A : Type) := { val : A }.
Lemma usetc {t : class nat} : P (@val nat t).
Admitted.
Notation "{val:= v }" := (@val _ v).
Instance zero : class nat := {| val := 0 |}.
Lemma test : P 0.
Fail apply usetc.
pose (tmp := usetc); apply tmp; clear tmp.
Qed.
¤ Dauer der Verarbeitung: 0.0 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.
|
