summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2015-07-02 16:06:02 -0700
committerGravatar Rustan Leino <unknown>2015-07-02 16:06:02 -0700
commite10098cde7bac9a7a1576000fa29d15f1fcd8970 (patch)
tree424cc0d382c4f870fa133c18228809da4d6a1bea /Test/VSI-Benchmarks
parentc7f6887e452cbb91a8297bb64db39a8066750351 (diff)
Type parameters in method/function signatures are no longer auto-declared. Although
convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous.
Diffstat (limited to 'Test/VSI-Benchmarks')
0 files changed, 0 insertions, 0 deletions