|
Set Universe Polymorphism.
Record Pred@{A} :=
{ car :> Type@{A}
; P : car -> Prop
}.
Class All@{A} (A : Pred@{A}) : Type :=
{ proof : forall (a : A), P A a
}.
Record Pred_All@{A} : Type :=
{ P' :> Pred@{A}
; P'_All : All P'
}.
Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
Proof.
solve[auto using proof].
Abort.
¤ Dauer der Verarbeitung: 0.14 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.
|
