Clean up/add warnings to use of triggers

dafny-lang / libraries

Libraries useful for Dafny programs

Other

43 stars 25 forks source link

Clean up/add warnings to use of triggers #17

Open robin-aws opened 3 years ago

robin-aws commented 3 years ago

Follow-up from https://github.com/dafny-lang/libraries/pull/7#issuecomment-909412689: 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 commented 3 years ago

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.