Inconsistent {:newType}
and {:newType true}
#1919
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: documentation
Dafny's reference manual, tutorial, and other materials
part: language definition
Relating to the Dafny language definition itself
To be consistent with other attributes,
{:nativeType}
and{:nativeType true}
should do the same thing.Currently, the documentation says:
{:nativeType}
- With no parameters it has no effect and theNewtypeDecl
will have its default behavior which is to choose a native type that can hold any
value satisfying the constraints, if possible, otherwise BigInteger is used.
{:nativeType true}
- Also gives defaultNewtypeDecl
behavior,but gives an error if base type is not integral.
The text was updated successfully, but these errors were encountered: