|
Record foo := { f : Type }.
Fail Canonical Structure xx@{} := {| f := Type |}.
Canonical Structure xx@{i} := {| f := Type@{i} |}.
Fail Coercion cc@{} := fun x : Type => Build_foo x.
Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x.
Coercion cc1@{i} := (cc@{i}).
¤ Dauer der Verarbeitung: 0.12 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.
|
