Polymorphic Definition foo@{u|} (A : Type@{u}) (a b: A) (p : a = b) : True := match p in (_ = a1) with
| eq_refl => I end. (* Universe constraints are not implied by the ones declared: u <= eq.u0 *)
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.
