Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Inconsistent {:newType} and {:newType true} #1919

Open
MikaelMayer opened this issue Mar 18, 2022 · 0 comments
Open

Inconsistent {:newType} and {:newType true} #1919

MikaelMayer opened this issue Mar 18, 2022 · 0 comments
Assignees
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

Comments

@MikaelMayer
Copy link
Member

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 the NewtypeDecl
    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 default NewtypeDecl behavior,
    but gives an error if base type is not integral.
@MikaelMayer MikaelMayer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself labels Mar 18, 2022
@davidcok davidcok added the part: documentation Dafny's reference manual, tutorial, and other materials label Jul 15, 2022
@davidcok davidcok self-assigned this Apr 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Projects
None yet
Development

No branches or pull requests

2 participants