|
(* A type, not a class *)
Variant T := mkT.
(* In records, :> declares a coercion *)
Record R := { t_of_r :> T }.
Check forall r : R, r = r :> T.
(* A class *)
Class A := { p : Prop }.
(* A sub-class *)
Class B := { a_of_b :> A ; t_of_b :> T }.
(* The sub-instance is automatically inferred due to :> for a_of_b *)
Check forall b : B, p.
(* No coercion is introduced by :> in t_of_b *)
Fail Check forall b : B, b = b :> T.
(* Using :> when the RHS is not a class produces a “not-a-class” warning. *)
Set Warnings "+not-a-class".
Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }.
¤ Dauer der Verarbeitung: 0.15 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.
|
