|
Set Implicit Arguments.
Unset Strict Implicit.
Module OK.
Record A := mkA {
T : Type;
P : T -> bool;
}.
About P. (* Argument a is implicit *)
Check P (true: T (mkA negb)).
End OK.
Module KO.
Set Primitive Projections.
Record A := mkA {
T : Type;
P : T -> bool;
}.
About P. (* No implicit arguments *)
Check P (true: T (mkA negb)).
(*
The command has indeed failed with message:
The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}"
while it is expected to have type "A".
*)
End KO.
¤ Dauer der Verarbeitung: 0.15 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.
|
