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

Clean up/add warnings to use of triggers #17

Open
robin-aws opened this issue Sep 29, 2021 · 1 comment
Open

Clean up/add warnings to use of triggers #17

robin-aws opened this issue Sep 29, 2021 · 1 comment
Labels
usability Improvements to the usability of the libraries

Comments

@robin-aws
Copy link
Member

robin-aws commented Sep 29, 2021

Follow-up from #7 (comment): we agree that while it is reasonable for a Dafny standard library to make limited use of triggers, we want to ensure that Dafny programmers are strongly encouraged to avoid triggers in their own code.

@parno
Copy link
Contributor

parno commented Oct 27, 2021

This is currently waiting on PR #25, which in turn is waiting on review from @RustanLeino. Once that lands, @sydgibs has a follow on set of patches to add triggers to the rest of the library.

@atomb atomb added the usability Improvements to the usability of the libraries label Apr 20, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
usability Improvements to the usability of the libraries
Projects
None yet
Development

No branches or pull requests

3 participants