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.

Sign up for GitHub

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

Jump to bottom

Support attributes on parameters #5032

Closed
keyboardDrummer opened this issue Jan 31, 2024 · 0 comments · Fixed by #5036
Closed

Support attributes on parameters #5032

keyboardDrummer opened this issue Jan 31, 2024 · 0 comments · Fixed by #5036
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jan 31, 2024 •
edited
Loading

Dafny currently does not support attributes on parameters. Allowing attributes here is useful for custom back-ends that may wish to annotate parameters to customize code generation

Example:

function Foo({:should-be-possible} x: int): int {
  3
}

datatype A = A({:should-be-possible} x: int)
@keyboardDrummer keyboardDrummer added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jan 31, 2024
@keyboardDrummer keyboardDrummer mentioned this issue Feb 1, 2024
Merged
keyboardDrummer added a commit that referenced this issue Feb 2, 2024
@keyboardDrummer
Parameter attributes (#5036)
c6cd10d 
Fixes #5032

### Description
Support attributes in parameters

### How has this been tested?
Updated an existing littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Parameter attributes keyboardDrummer/dafny
1 participant
@keyboardDrummer