index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
/
triggers
Mode
Name
Size
-rw-r--r--
auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
979
log
plain
-rw-r--r--
auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
213
log
plain
-rw-r--r--
constructors-cause-matching-loops.dfy
351
log
plain
-rw-r--r--
constructors-cause-matching-loops.dfy.expect
251
log
plain
-rw-r--r--
function-applications-are-triggers.dfy
583
log
plain
-rw-r--r--
function-applications-are-triggers.dfy.expect
687
log
plain
-rw-r--r--
large-quantifiers-dont-break-dafny.dfy
2074
log
plain
-rw-r--r--
large-quantifiers-dont-break-dafny.dfy.expect
627
log
plain
-rw-r--r--
loop-detection-is-not-too-strict.dfy
1834
log
plain
-rw-r--r--
loop-detection-is-not-too-strict.dfy.expect
1116
log
plain
-rw-r--r--
loop-detection-looks-at-ranges-too.dfy
524
log
plain
-rw-r--r--
loop-detection-looks-at-ranges-too.dfy.expect
421
log
plain
-rw-r--r--
loop-detection-messages--unit-tests.dfy
1254
log
plain
-rw-r--r--
loop-detection-messages--unit-tests.dfy.expect
3014
log
plain
-rw-r--r--
looping-is-hard-to-decide-modulo-equality.dfy
1246
log
plain
-rw-r--r--
looping-is-hard-to-decide-modulo-equality.dfy.expect
571
log
plain
-rw-r--r--
matrix-accesses-are-triggers.dfy
372
log
plain
-rw-r--r--
matrix-accesses-are-triggers.dfy.expect
496
log
plain
-rw-r--r--
nested-quantifiers-all-get-triggers.dfy
374
log
plain
-rw-r--r--
nested-quantifiers-all-get-triggers.dfy.expect
225
log
plain
-rw-r--r--
old-is-a-special-case-for-triggers.dfy
1489
log
plain
-rw-r--r--
old-is-a-special-case-for-triggers.dfy.expect
1098
log
plain
-rw-r--r--
redundancy-detection-is-bidirectional.dfy
1133
log
plain
-rw-r--r--
redundancy-detection-is-bidirectional.dfy.expect
795
log
plain
-rw-r--r--
regression-tests.dfy
716
log
plain
-rw-r--r--
regression-tests.dfy.expect
133
log
plain
-rw-r--r--
set-construction-is-a-good-trigger.dfy
657
log
plain
-rw-r--r--
set-construction-is-a-good-trigger.dfy.expect
304
log
plain
-rw-r--r--
some-proofs-only-work-without-autoTriggers.dfy
2007
log
plain
-rw-r--r--
some-proofs-only-work-without-autoTriggers.dfy.expect
1276
log
plain
-rw-r--r--
some-terms-do-not-look-like-the-triggers-they-match.dfy
809
log
plain
-rw-r--r--
some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
750
log
plain
-rw-r--r--
splitting-picks-the-right-tokens.dfy
745
log
plain
-rw-r--r--
splitting-picks-the-right-tokens.dfy.expect
2084
log
plain
-rw-r--r--
splitting-triggers-recovers-expressivity.dfy
1778
log
plain
-rw-r--r--
splitting-triggers-recovers-expressivity.dfy.expect
2253
log
plain
-rw-r--r--
splitting-triggers-yields-better-precondition-related-errors.dfy
505
log
plain
-rw-r--r--
splitting-triggers-yields-better-precondition-related-errors.dfy.expect
2159
log
plain
-rw-r--r--
suppressing-warnings-behaves-properly.dfy
808
log
plain
-rw-r--r--
suppressing-warnings-behaves-properly.dfy.expect
1509
log
plain
-rw-r--r--
triggers-prevent-some-inlining.dfy
1079
log
plain
-rw-r--r--
triggers-prevent-some-inlining.dfy.expect
765
log
plain
-rw-r--r--
useless-triggers-are-removed.dfy
930
log
plain
-rw-r--r--
useless-triggers-are-removed.dfy.expect
858
log
plain
-rw-r--r--
wf-checks-use-the-original-quantifier.dfy
1309
log
plain
-rw-r--r--
wf-checks-use-the-original-quantifier.dfy.expect
945
log
plain