/Test/triggers/

• ../
• auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
• auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
• constructors-cause-matching-loops.dfy
• constructors-cause-matching-loops.dfy.expect
• function-applications-are-triggers.dfy
• function-applications-are-triggers.dfy.expect
• large-quantifiers-dont-break-dafny.dfy
• large-quantifiers-dont-break-dafny.dfy.expect
• loop-detection-is-not-too-strict.dfy
• loop-detection-is-not-too-strict.dfy.expect
• loop-detection-looks-at-ranges-too.dfy
• loop-detection-looks-at-ranges-too.dfy.expect
• loop-detection-messages--unit-tests.dfy
• loop-detection-messages--unit-tests.dfy.expect
• looping-is-hard-to-decide-modulo-equality.dfy
• looping-is-hard-to-decide-modulo-equality.dfy.expect
• matrix-accesses-are-triggers.dfy
• matrix-accesses-are-triggers.dfy.expect
• nested-quantifiers-all-get-triggers.dfy
• nested-quantifiers-all-get-triggers.dfy.expect
• old-is-a-special-case-for-triggers.dfy
• old-is-a-special-case-for-triggers.dfy.expect
• redundancy-detection-is-bidirectional.dfy
• redundancy-detection-is-bidirectional.dfy.expect
• regression-tests.dfy
• regression-tests.dfy.expect
• set-construction-is-a-good-trigger.dfy
• set-construction-is-a-good-trigger.dfy.expect
• some-proofs-only-work-without-autoTriggers.dfy
• some-proofs-only-work-without-autoTriggers.dfy.expect
• some-terms-do-not-look-like-the-triggers-they-match.dfy
• some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
• splitting-picks-the-right-tokens.dfy
• splitting-picks-the-right-tokens.dfy.expect
• splitting-triggers-recovers-expressivity.dfy
• splitting-triggers-recovers-expressivity.dfy.expect
• splitting-triggers-yields-better-precondition-related-errors.dfy
• splitting-triggers-yields-better-precondition-related-errors.dfy.expect
• suppressing-warnings-behaves-properly.dfy
• suppressing-warnings-behaves-properly.dfy.expect
• triggers-prevent-some-inlining.dfy
• triggers-prevent-some-inlining.dfy.expect
• useless-triggers-are-removed.dfy
• useless-triggers-are-removed.dfy.expect
• wf-checks-use-the-original-quantifier.dfy
• wf-checks-use-the-original-quantifier.dfy.expect