|
(** 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 of inductive t. *)
¤ 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.
|
