Definition t1@{s;u|} (A:Type@{s;u}) (x y : A) := box _ x. Definition t2@{s;u|} (A:Type@{s;u}) (x y : A) := box _ y.
Checkfun A:SProp => eq_refl : t1 A = t2 A. (* What is in "test-suite/success/sort_polymorphism.v" *) Checkfun (A : SProp) => (fun (x : t1 A = t2 A) => x) eq_refl. (* Slight variation *)
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.
