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

Allow specifying pre/post on trait definitions #731

Closed
W95Psp opened this issue Jun 20, 2024 · 0 comments · Fixed by #790
Closed

Allow specifying pre/post on trait definitions #731

W95Psp opened this issue Jun 20, 2024 · 0 comments · Fixed by #790
Assignees
@W95Psp
Labels
engine Issue in the engine

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Jun 20, 2024 •
edited
Loading

Currently, every function of every trait has a pre/post that instances can implement.
On the trait level, it is currently not possible to add a pre or postcondition.
@W95Psp W95Psp added the engine Issue in the engine label Jun 21, 2024
@W95Psp W95Psp self-assigned this Jul 11, 2024
W95Psp added a commit that referenced this issue Jul 18, 2024
@W95Psp
feat: allow pre/post on traits (fixes #731)
d6f5beb
@W95Psp W95Psp mentioned this issue Jul 18, 2024
Merged
@W95Psp W95Psp closed this as completed Jul 22, 2024
@github-project-automation github-project-automation bot moved this to Done in hax Jul 22, 2024
W95Psp added a commit that referenced this issue Jul 22, 2024
@W95Psp
feat: allow pre/post on traits (fixes #731)
93cc58d
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@W95Psp W95Psp

Labels
engine Issue in the engine
Projects
No open projects
hax
Status: Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Allow ensures and requires on traits hacspec/hax
1 participant
@W95Psp