| .. |
|
Issue4569
|
d1b41cc4d4
[ #4569 ] MWE for failure of Mac OS X install with dynamic linking
|
4 years ago |
|
fixed
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
Issue2636.agda
|
2f212bf556
Add --auto-inline and make it off by default
|
4 years ago |
|
Issue2636.err
|
2f212bf556
Add --auto-inline and make it off by default
|
4 years ago |
|
Issue3027.agda
|
935523f9c7
[ revert 3c6482b ] Revert fix for #3027 (pr #4392) for the sake of #4408
|
5 years ago |
|
Issue3027.err
|
50dd519271
Replace "file and line" with CallStack for errors
|
4 years ago |
|
Issue3027b.agda
|
935523f9c7
[ revert 3c6482b ] Revert fix for #3027 (pr #4392) for the sake of #4408
|
5 years ago |
|
Issue3027b.err
|
50dd519271
Replace "file and line" with CallStack for errors
|
4 years ago |
|
Issue325b.agda
|
0f19b421a2
[ test/Bugs ] remove debug output from Issue325b
|
5 years ago |
|
Issue325b.err
|
552987aa01
More fine-grained blocking (#4782)
|
4 years ago |
|
Issue3898.agda
|
15d8f7ed15
Test cases for forcing issues
|
5 years ago |
|
Issue3898.err
|
c445e699d8
[ enhance ] Use distinct exit codes for TCM errors, impossibles, etc.
|
4 years ago |
|
Issue4251.agda
|
f9a922c5fd
add #4251 test case to test/Bugs
|
4 years ago |
|
Issue4251.err
|
f9a922c5fd
add #4251 test case to test/Bugs
|
4 years ago |
|
Issue4755b.agda
|
6f743f15e1
[ re #4755 ] Add dummy terms for missing parameters when applying rewrite rule on constructor term
|
4 years ago |
|
Issue4755b.err
|
6f743f15e1
[ re #4755 ] Add dummy terms for missing parameters when applying rewrite rule on constructor term
|
4 years ago |
|
Issue5007-sizedtypes.agda
|
043f62bec1
[ re #4727 ] Add sized types example to test/Bugs
|
4 years ago |
|
Issue5007-sizedtypes.err
|
043f62bec1
[ re #4727 ] Add sized types example to test/Bugs
|
4 years ago |
|
LongList.agda
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
MisspelledKeywordInRecord.agda
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
MisspelledKeywordInRecord.err
|
c445e699d8
[ enhance ] Use distinct exit codes for TCM errors, impossibles, etc.
|
4 years ago |
|
NakedEllipsisWeirdError.agda
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
NakedEllipsisWeirdError.err
|
c445e699d8
[ enhance ] Use distinct exit codes for TCM errors, impossibles, etc.
|
4 years ago |
|
NonRecursiveCoinductiveRecord.agda
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
SizedTypesLoopDueInadmissibility.agda
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
SizedTypesScopeViolationInMeta.err
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
|
Tests.hs
|
8ca2402d1f
Testsuite: use Text.words consistently when diffing
|
3 years ago |
|
bugs.agda-lib
|
08dd23df8d
[ fix #3129 ] add 'bugs' target to the test suite (#3970)
|
5 years ago |
Andreas Abel
8ca2402d1f
Testsuite: use Text.words consistently when diffing