(* :> declares a coercion *)
Record R := { t_of_r :> T }. Checkforall 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 *) Checkforall b : B, p. (* No coercion is introduced by :> in t_of_b *)
Fail Checkforall 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 }.
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.
