|
Set Primitive Projections.
Record unit : Set := tt {}.
Fail Check fun x : unit => eq_refl : tt = x.
Fail Check fun x : unit => eq_refl : x = tt.
Fail Check fun x y : unit => (eq_refl : x = tt) : x = y.
Fail Check fun x y : unit => eq_refl : x = y.
Record ok : Set := tt' { a : unit }.
Record nonprim : Prop := { undef : unit }.
Record prim : Prop := { def : True }.
¤ Dauer der Verarbeitung: 0.16 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.
|
