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.
robin-aws
commented
2 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.