|
Set Universe Polymorphism.
Record Type_Over (X : Type)
:= { Domain :> Type;
proj : Domain -> X }.
Definition Self_Over (X : Type)
:= {| Domain := X; proj := (fun x => x) |}.
Canonical Structure Self_Over. (* fails with Anomaly: Mismatched instance and context when building universe substitution. Please report. for polymorphic structures *)
(* if monomorphic, Warning: No global reference exists for projection
valuefun x : _UNBOUND_REL_1 => x in instance Self_Over of proj, ignoring it. *)
¤ Dauer der Verarbeitung: 0.13 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.
|
