(** Check that various errors in record fields are reported with the correct
underlying issue. *)
Record t :=
{ foo: unit }.
Record t' :=
{ bar: unit }.
Fail Check {| unit := tt |}. (* unit: Not a projection. *)
Fail Check {| unit := tt;
foo := tt |}. (* unit: Not a projection. *)
Fail Check {| foo := tt;
bar := tt |}. (* This record contains fields of both t and t'. *)
Fail Check {| unit := tt;
unit := tt |}. (* unit: Not a projection. *)
Fail Check {| foo := tt;
foo := tt |}. (* This record defines several times the field foo. *)
Fail Check {| foo := tt;
unit := tt;
unit := tt |}. (* This is slightly wrong (would prefer "unit: Not a projection."), but it's
acceptable and seems an unlikely mistake. *) (* This record defines several times the field unit. *)
Fail Check {| foo := tt;
unit := tt |}. (* unit: Not a projection. *)
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.
