| .. |
|
Issue2486
|
3b3034a669
[ #2486 ] test case extension and simplification
|
пре 7 година |
|
Issue561
|
c96a34dfc8
Removed deprecated UHC pragramas and FloatsUHCFails test.
|
пре 4 година |
|
Lib
|
df563b2c57
[ compiler test ] cosmetics
|
пре 5 година |
|
Arith.agda
|
98f7d8dec9
[ fixed #1854 ] work-arounds for #1855 #1856 #1857 to get compiler-tests passing
|
пре 8 година |
|
Arith.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
BuiltinInt.agda
|
a10f892af5
[ test ] compiler test for builtin integers
|
пре 9 година |
|
BuiltinInt.out
|
a10f892af5
[ test ] compiler test for builtin integers
|
пре 9 година |
|
CaseOnCase.agda
|
c96a34dfc8
Removed deprecated UHC pragramas and FloatsUHCFails test.
|
пре 4 година |
|
CaseOnCase.out
|
72a51dcc28
[ #4967 ] test case
|
пре 4 година |
|
CatchAllVarArity.agda
|
ee58fe2a52
[ MAlonzo ] compiles now from case trees if they do not have catch-alls.
|
пре 9 година |
|
CatchAllVarArity.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Coind.agda
|
e205a43e87
Fixed #1209.
|
пре 6 година |
|
Coind.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
CompareNat.agda
|
a50ff581f3
[ #2487 ] consistency checking of options
|
пре 5 година |
|
CompareNat.out
|
5685f07d19
[ treeless ] don't print unreachable catch-all clauses
|
пре 8 година |
|
CompileAsPattern.agda
|
ca3f66da8d
[ #3732 ] remove Treeless output; differs now between MAlonzo and JA
|
пре 5 година |
|
CompileAsPattern.out
|
ca3f66da8d
[ #3732 ] remove Treeless output; differs now between MAlonzo and JA
|
пре 5 година |
|
CompileCatchAll.agda
|
437b867f54
[ treeless ] improved compilation of catch-all clauses
|
пре 8 година |
|
CompileCatchAll.out
|
112e498b99
Merge branch 'stable-2.5'
|
пре 7 година |
|
CompileNumbers.agda
|
b5e862bbfb
fixed compiler tests broken by previous commit
|
пре 8 година |
|
CompileNumbers.out
|
e3bfa63444
[ treeless ] implement analysis of unreachable branches for int/nat cases
|
пре 7 година |
|
CompiledRecord.agda
|
b56b3965a6
[ backend ] updated compiler pragmas in test cases
|
пре 7 година |
|
CompiledRecord.out
|
182b6d6a8f
[ tests ] Move some compiler tests from Succeed to Compiler/simple.
|
пре 9 година |
|
CompilingCoinduction.agda
|
0fc6b558b0
[ re #5386 ] Address two comments by @nad
|
пре 3 година |
|
CompilingCoinduction.out
|
329af16c11
[ tests ] Move some compiler tests from succeed to Compiler/simple .
|
пре 9 година |
|
CompilingQNamePats.agda
|
329af16c11
[ tests ] Move some compiler tests from succeed to Compiler/simple .
|
пре 9 година |
|
CompilingQNamePats.out
|
329af16c11
[ tests ] Move some compiler tests from succeed to Compiler/simple .
|
пре 9 година |
|
CopatternRecord.agda
|
ee58fe2a52
[ MAlonzo ] compiles now from case trees if they do not have catch-alls.
|
пре 9 година |
|
CopatternRecord.out
|
ee58fe2a52
[ MAlonzo ] compiles now from case trees if they do not have catch-alls.
|
пре 9 година |
|
CopatternStreamSized.agda
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
пре 3 година |
|
CopatternStreamSized.out
|
03c8272555
[ js ] Enable some more tests
|
пре 7 година |
|
Cubical-is-not-supported.agda
|
98251e6c51
[ #4701 ] The GHC and JS backends now reject cubical code.
|
пре 3 година |
|
Cubical-is-not-supported.out
|
98251e6c51
[ #4701 ] The GHC and JS backends now reject cubical code.
|
пре 3 година |
|
Cubical-primitives-are-not-supported.agda
|
5894deccb3
[ #4638 ] The GHC and JS backends are now more picky.
|
пре 4 година |
|
Cubical-primitives-are-not-supported.out
|
98251e6c51
[ #4701 ] The GHC and JS backends now reject cubical code.
|
пре 3 година |
|
EraseRefl.agda
|
86ca8dc8cc
[ treeless ] changed debug output
|
пре 9 година |
|
EraseRefl.out
|
112e498b99
Merge branch 'stable-2.5'
|
пре 7 година |
|
Erased-constructors.agda
|
95e36742e3
[ #4638 ] skip erased declarations in JS compilation
|
пре 3 година |
|
Erased-constructors.out
|
f9a8ca1d1a
[ #4638 ] Tests.
|
пре 4 година |
|
Erased-cubical-Cubical.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical-Cubical.options
|
7181c83f23
[ #4701 ] Added support for --erased-cubical to the GHC backend.
|
пре 3 година |
|
Erased-cubical-FFI.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical-FFI.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Erased-cubical-FFI.out
|
7181c83f23
[ #4701 ] Added support for --erased-cubical to the GHC backend.
|
пре 3 година |
|
Erased-cubical-Pattern-matching-Cubical.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical-Pattern-matching-Cubical.options
|
ed4584a1c6
[ #4701 ] Added --erased-cubical.
|
пре 3 година |
|
Erased-cubical-Pattern-matching-Erased.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical-Pattern-matching-Erased.options
|
ed4584a1c6
[ #4701 ] Added --erased-cubical.
|
пре 3 година |
|
Erased-cubical-Pattern-matching.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical-Pattern-matching.out
|
ed4584a1c6
[ #4701 ] Added --erased-cubical.
|
пре 3 година |
|
Erased-cubical.agda
|
b52a21df38
[ #5731 ] Added --save-metas and --no-save-metas.
|
пре 2 година |
|
Erased-cubical.out
|
7181c83f23
[ #4701 ] Added support for --erased-cubical to the GHC backend.
|
пре 3 година |
|
Erasure-Issue2640.agda
|
f3c38bca0f
[ #2757 ] an attempt to address issue #2640 for runtime-erasure
|
пре 6 година |
|
Erasure-Issue2640.out
|
f3c38bca0f
[ #2757 ] an attempt to address issue #2640 for runtime-erasure
|
пре 6 година |
|
ExportAndUse.agda
|
b56b3965a6
[ backend ] updated compiler pragmas in test cases
|
пре 7 година |
|
ExportAndUse.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
ExportAndUse.out
|
1c9c68117f
[ fixes #2584 ] print warnings before finalizer
|
пре 7 година |
|
FFI.agda
|
5803c1c393
[ ghc-backend ] make it possible to preserve polymorphic types in type approximations
|
пре 7 година |
|
FFI.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
FFI.out
|
957903a466
[ ghc ] Allow COMPILED pragma on functions.
|
пре 7 година |
|
FlexibleInterpreter.agda
|
cc0e38df20
[ #1918 ] Removed unnecessary occurrences of `no-coverage-check`.
|
пре 8 година |
|
FlexibleInterpreter.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Floats.agda
|
0f4538c8dc
First step of float revision (see #4868)
|
пре 4 година |
|
Floats.out
|
0f4538c8dc
First step of float revision (see #4868)
|
пре 4 година |
|
Forcing.agda
|
df563b2c57
[ compiler test ] cosmetics
|
пре 5 година |
|
Forcing.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Forcing2.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Forcing2.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Forcing3.agda
|
df563b2c57
[ compiler test ] cosmetics
|
пре 5 година |
|
Forcing3.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Forcing4.agda
|
df563b2c57
[ compiler test ] cosmetics
|
пре 5 година |
|
Forcing4.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
HOAny.agda
|
a1090c4e99
[ fix #3696 ] AgdaAny should be poly-kinded (#3706)
|
пре 5 година |
|
HOAny.out
|
a1090c4e99
[ fix #3696 ] AgdaAny should be poly-kinded (#3706)
|
пре 5 година |
|
HelloWorld.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
HelloWorld.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Higher-inductive-types-are-not-supported.agda
|
5894deccb3
[ #4638 ] The GHC and JS backends are now more picky.
|
пре 4 година |
|
Higher-inductive-types-are-not-supported.out
|
98251e6c51
[ #4701 ] The GHC and JS backends now reject cubical code.
|
пре 3 година |
|
IdentitySmashing.agda
|
ca3f66da8d
[ #3732 ] remove Treeless output; differs now between MAlonzo and JA
|
пре 5 година |
|
IdentitySmashing.out
|
ca3f66da8d
[ #3732 ] remove Treeless output; differs now between MAlonzo and JA
|
пре 5 година |
|
InlineRecursive.agda
|
f4982e5ca5
[ test ] test that inlining a recursive function doesn't loop the compiler
|
пре 9 година |
|
InlineRecursive.out
|
74a5c72d1e
[ treeless ] don't inline variables with atomic values
|
пре 7 година |
|
Irrelevant.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Irrelevant.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Issue1126.agda
|
4f77f328e8
Re #1126 fix JS compilation
|
пре 7 година |
|
Issue1126.out
|
81a92d5ace
Issue #1126 is fixed (compiler optimization in GHC backend)
|
пре 7 година |
|
Issue1252.agda
|
b56b3965a6
[ backend ] updated compiler pragmas in test cases
|
пре 7 година |
|
Issue1252.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue1252.out
|
00c47f7fca
[ compiler test ] include output for compile-only tests
|
пре 7 година |
|
Issue1441.agda
|
d03adfbc73
[ tests ] Move epic test to Compiler tests.
|
пре 9 година |
|
Issue1441.out
|
d03adfbc73
[ tests ] Move epic test to Compiler tests.
|
пре 9 година |
|
Issue1486.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Issue1486.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Issue1496.agda
|
1d0bf065c3
[ test ] removed Common/FFI.hs (no longer needed)
|
пре 8 година |
|
Issue1496.out
|
c9ce8fdbb0
[ tests ] Forgot to move some tests during renaming.
|
пре 9 година |
|
Issue1624.agda
|
77749d00b5
[ Issue #1624 ] Fixed by dropping case scrutinee from environment in literal branches.
|
пре 9 година |
|
Issue1624.out
|
77749d00b5
[ Issue #1624 ] Fixed by dropping case scrutinee from environment in literal branches.
|
пре 9 година |
|
Issue1632.agda
|
9d7c9b2b55
[ tests ] Use standard IO instead of MAlonzo specific functions.
|
пре 9 година |
|
Issue1632.out
|
182b6d6a8f
[ tests ] Move some compiler tests from Succeed to Compiler/simple.
|
пре 9 година |
|
Issue1664.agda
|
d44fc042f1
[ fixed #3991 ] allow fractional precedences in fixity declarations
|
пре 5 година |
|
Issue1664.out
|
d44fc042f1
[ fixed #3991 ] allow fractional precedences in fixity declarations
|
пре 5 година |
|
Issue1855.agda
|
0cc81873ad
[ Fix #1855 ] Normalize concrete names in UHC backend.
|
пре 8 година |
|
Issue1855.out
|
0cc81873ad
[ Fix #1855 ] Normalize concrete names in UHC backend.
|
пре 8 година |
|
Issue2123.agda
|
424702da8b
[ fixed #2123 ] treeless optimizer erasing too much
|
пре 8 година |
|
Issue2123.out
|
424702da8b
[ fixed #2123 ] treeless optimizer erasing too much
|
пре 8 година |
|
Issue2218.agda
|
c86cbe03c4
[ test-suite ] Renamed `nan` to `NaN` and `inf` to `Inf`.
|
пре 8 година |
|
Issue2218.out
|
0f4538c8dc
First step of float revision (see #4868)
|
пре 4 година |
|
Issue2222.agda
|
77a85e5552
[ js, fix #2222 ] Make JS IO monad lazy.
|
пре 8 година |
|
Issue2222.out
|
77a85e5552
[ js, fix #2222 ] Make JS IO monad lazy.
|
пре 8 година |
|
Issue223.agda
|
b56b3965a6
[ backend ] updated compiler pragmas in test cases
|
пре 7 година |
|
Issue223.hs
|
c9ce8fdbb0
[ tests ] Forgot to move some tests during renaming.
|
пре 9 година |
|
Issue223.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue223.out
|
00c47f7fca
[ compiler test ] include output for compile-only tests
|
пре 7 година |
|
Issue2469.agda
|
fb6ff2ff05
Revert "[ common test files ] Renamed Common.Product to Common.Sigma."
|
пре 6 година |
|
Issue2469.out
|
797ea79162
[ fix #2469 ] Fix varying arity treeless compilation.
|
пре 7 година |
|
Issue2486.agda
|
3b3034a669
[ #2486 ] test case extension and simplification
|
пре 7 година |
|
Issue2486.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue2486.out
|
889771c797
[ fix #2486 ] Fix foreign data inheritance problem.
|
пре 7 година |
|
Issue2524.agda
|
0a8f7bbafb
[ #2524 ] Fix test case for JS backend.
|
пре 7 година |
|
Issue2524.out
|
dae17decf2
Re #2524: allow arbitrary GHC compilation of abstract defs
|
пре 7 година |
|
Issue2664.agda
|
f1c2104c0a
Fixed #2664: do not record pattern translate projection defs
|
пре 7 година |
|
Issue2664.out
|
f1c2104c0a
Fixed #2664: do not record pattern translate projection defs
|
пре 7 година |
|
Issue2712.agda
|
be3f8af9f6
Fixed #2714 --no-main is now a pragma option
|
пре 7 година |
|
Issue2712.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue2712.out
|
be3f8af9f6
Fixed #2714 --no-main is now a pragma option
|
пре 7 година |
|
Issue2714.agda
|
be3f8af9f6
Fixed #2714 --no-main is now a pragma option
|
пре 7 година |
|
Issue2714.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue2714.out
|
834c77ac49
Re #2714 forgot test output
|
пре 7 година |
|
Issue2821.agda
|
fda20b721b
[ fixed #2382 ] builtin NIL and CONS no longer needed
|
пре 7 година |
|
Issue2821.out
|
86eb792a27
[ fix #2783 ] Most builtin modules may use postulates and still be safe
|
пре 5 година |
|
Issue2879-1.agda
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
пре 3 година |
|
Issue2879-1.out
|
d95179b987
Fixed #2879.
|
пре 6 година |
|
Issue2879-2.agda
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
пре 3 година |
|
Issue2879-2.out
|
d95179b987
Fixed #2879.
|
пре 6 година |
|
Issue2909-1.agda
|
e205a43e87
Fixed #1209.
|
пре 6 година |
|
Issue2909-1.out
|
4f46750db4
[ #2909 ] Test cases.
|
пре 6 година |
|
Issue2909-2.agda
|
e205a43e87
Fixed #1209.
|
пре 6 година |
|
Issue2909-2.out
|
4f46750db4
[ #2909 ] Test cases.
|
пре 6 година |
|
Issue2909-4.agda
|
e205a43e87
Fixed #1209.
|
пре 6 година |
|
Issue2909-4.out
|
4f46750db4
[ #2909 ] Test cases.
|
пре 6 година |
|
Issue2909-5.agda
|
da1a77c650
Fixed #2909.
|
пре 6 година |
|
Issue2909-5.out
|
c445e699d8
[ enhance ] Use distinct exit codes for TCM errors, impossibles, etc.
|
пре 4 година |
|
Issue2909-6.agda
|
da1a77c650
Fixed #2909.
|
пре 6 година |
|
Issue2909-6.out
|
c445e699d8
[ enhance ] Use distinct exit codes for TCM errors, impossibles, etc.
|
пре 4 година |
|
Issue2914.agda
|
5434f70391
[ fixed #2914 ] don't dead-code eliminate definitions with compiler pragmas
|
пре 6 година |
|
Issue2914.out
|
5434f70391
[ fixed #2914 ] don't dead-code eliminate definitions with compiler pragmas
|
пре 6 година |
|
Issue2918-Inlining.agda
|
191427acd9
[ #2918 ] Added a test case.
|
пре 4 година |
|
Issue2918-Inlining.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue2918-Inlining.out
|
191427acd9
[ #2918 ] Added a test case.
|
пре 4 година |
|
Issue2918.agda
|
941676bc19
Fixed #2931: Renamed Agda.Builtin.Size.ω to ∞.
|
пре 6 година |
|
Issue2918.out
|
09f4c86884
[ #2918 ] Test case.
|
пре 6 година |
|
Issue2921.agda
|
53de225445
[ fixed #3732 ] GHC backend: No erasure for types with a COMPILE binding
|
пре 5 година |
|
Issue2921.out
|
510242e24c
[ fixed #2921 ] handle compile-data pragmas in the presence of erased constructor args
|
пре 6 година |
|
Issue3045.agda
|
03d874b8e5
Re #3045 fix JS compilation
|
пре 6 година |
|
Issue3045.out
|
301ac90269
[ fixed #3045 ] generate enough extra arguments in GHC backend
|
пре 6 година |
|
Issue326.agda
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Issue326.out
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Issue3380.agda
|
f5fb43467f
[ fix #3380 ] don't erase lambdas into erased terms if strict backend
|
пре 5 година |
|
Issue3380.out
|
f5fb43467f
[ fix #3380 ] don't erase lambdas into erased terms if strict backend
|
пре 5 година |
|
Issue3410.agda
|
98d6f195fe
[ fix ] using Common.IO rather than postulates (#3472)
|
пре 6 година |
|
Issue3410.out
|
4efe14bbe3
[ fix #3410 ] iterate forcing translation as long as it's making progress
|
пре 6 година |
|
Issue3732.agda
|
53de225445
[ fixed #3732 ] GHC backend: No erasure for types with a COMPILE binding
|
пре 5 година |
|
Issue3732.out
|
53de225445
[ fixed #3732 ] GHC backend: No erasure for types with a COMPILE binding
|
пре 5 година |
|
Issue3886.agda
|
84f7ffe05e
[ fixed #3886 ] by adding origin to Quantity
|
пре 5 година |
|
Issue3886.out
|
84f7ffe05e
[ fixed #3886 ] by adding origin to Quantity
|
пре 5 година |
|
Issue4168-4185.agda
|
94afdea0bb
[ re #4390 ] Updated test cases
|
пре 4 година |
|
Issue4168-4185.out
|
5166a416e1
[ fixed #4168 (b) ] no uncurrying of metas over records with erased fields
|
пре 5 година |
|
Issue4168-shirr.agda
|
360c7a956e
[ fixed #4168 ] eta-contraction is unsound if all fields are unusable
|
пре 5 година |
|
Issue4168-shirr.out
|
360c7a956e
[ fixed #4168 ] eta-contraction is unsound if all fields are unusable
|
пре 5 година |
|
Issue4168.agda
|
360c7a956e
[ fixed #4168 ] eta-contraction is unsound if all fields are unusable
|
пре 5 година |
|
Issue4168.out
|
360c7a956e
[ fixed #4168 ] eta-contraction is unsound if all fields are unusable
|
пре 5 година |
|
Issue4169-2.agda
|
c2750993a1
[ #4169 ] Made more code work.
|
пре 5 година |
|
Issue4169-2.out
|
c2750993a1
[ #4169 ] Made more code work.
|
пре 5 година |
|
Issue4169.agda
|
fa63358de4
[ fixed #4169 ] MAlonzo: extra coercion needed when erased function is used
|
пре 5 година |
|
Issue4169.out
|
fa63358de4
[ fixed #4169 ] MAlonzo: extra coercion needed when erased function is used
|
пре 5 година |
|
Issue4638.agda
|
ced2905a41
[ #4638 ] Fixed some bugs.
|
пре 3 година |
|
Issue4638.out
|
ced2905a41
[ #4638 ] Fixed some bugs.
|
пре 3 година |
|
Issue4999.agda
|
9258d8c7d0
[ fix #4999 ] handle surrogate code points
|
пре 3 година |
|
Issue4999.out
|
9258d8c7d0
[ fix #4999 ] handle surrogate code points
|
пре 3 година |
|
Issue5288.agda
|
2bf7d55728
[ fixed #5288 ] treeless de Bruijn problem "withContextSize" (#5311)
|
пре 3 година |
|
Issue5288.out
|
2bf7d55728
[ fixed #5288 ] treeless de Bruijn problem "withContextSize" (#5311)
|
пре 3 година |
|
Issue5420.agda
|
35aa048075
[ JS backend ] Tried to fix #5420.
|
пре 3 година |
|
Issue5420.out
|
35aa048075
[ JS backend ] Tried to fix #5420.
|
пре 3 година |
|
Issue5421.agda
|
ef2d3d0957
[ GHC backend ] Tried to fix #5421.
|
пре 3 година |
|
Issue5421.out
|
ef2d3d0957
[ GHC backend ] Tried to fix #5421.
|
пре 3 година |
|
Issue5441.agda
|
4f95e08517
Fixed #5441.
|
пре 3 година |
|
Issue5441.options
|
4f95e08517
Fixed #5441.
|
пре 3 година |
|
Issue5441.out
|
4f95e08517
Fixed #5441.
|
пре 3 година |
|
Issue5602.agda
|
152efd679d
Fixed #5602.
|
пре 3 година |
|
Issue5602.out
|
152efd679d
Fixed #5602.
|
пре 3 година |
|
Issue561.agda
|
24da530fe3
[ fix #3483 ] by mimicking bindBuiltin's process (#3484)
|
пре 6 година |
|
Issue561.out
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Issue727.agda
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Issue727.out
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Issue728.agda
|
0fc6b558b0
[ re #5386 ] Address two comments by @nad
|
пре 3 година |
|
Issue728.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Issue728.out
|
5a5b9a2784
[ tests ] Use Haskell test runner for Succeed tests.
|
пре 9 година |
|
Literals.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Literals.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
ModuleArgs.agda
|
71e06cf88f
[ Fix #5425 ] Missing canonicalization crashes --js-optimize.
|
пре 3 година |
|
ModuleArgs.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
ModuleReexport.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
ModuleReexport.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Mutual.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Mutual.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
NoRecordConstructor.agda
|
51048bc3b6
[ MAlonzo ] Added a test for records without constructor.
|
пре 9 година |
|
NoRecordConstructor.out
|
51048bc3b6
[ MAlonzo ] Added a test for records without constructor.
|
пре 9 година |
|
PrimSeq.agda
|
b5e862bbfb
fixed compiler tests broken by previous commit
|
пре 8 година |
|
PrimSeq.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
PrimSeq.out
|
8e15d6d1e5
[ builtin ] new strictness primitives
|
пре 9 година |
|
PrintBool.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
PrintBool.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
QNameOrder.agda
|
82dd240c6f
[ compiler test ] added test for ordering of QNames
|
пре 8 година |
|
QNameOrder.out
|
82dd240c6f
[ compiler test ] added test for ordering of QNames
|
пре 8 година |
|
Records.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Records.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
Sharing.agda
|
c96a34dfc8
Removed deprecated UHC pragramas and FloatsUHCFails test.
|
пре 4 година |
|
Sharing.out
|
89707e1a90
[ compiler-tests ] Add test for sharing in generated code/runtime evaluation.
|
пре 9 година |
|
Sort.agda
|
98f7d8dec9
[ fixed #1854 ] work-arounds for #1855 #1856 #1857 to get compiler-tests passing
|
пре 8 година |
|
Sort.out
|
63a747240e
[ compiler test ] sorting the numbers 1199..0
|
пре 9 година |
|
StaticPatternLambda.agda
|
cb3e753001
[ treeless ] fixed issue with failed inlining of pattern lambdas
|
пре 9 година |
|
StaticPatternLambda.out
|
cb3e753001
[ treeless ] fixed issue with failed inlining of pattern lambdas
|
пре 9 година |
|
Strict.agda
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Strict.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
Strict.out
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
String.agda
|
017c22ec56
[ GHC ] Fix potential segfaults due to wrong primShowString.
|
пре 8 година |
|
String.out
|
2c0f465587
[ghc-backend] update test case to fixed primShowString
|
пре 7 година |
|
StringPattern.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
StringPattern.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
TrailingImplicits.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
TrailingImplicits.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
UniversePolymorphicIO.agda
|
d04e62b03c
[ prop ] Make Prop enabled by default
|
пре 6 година |
|
UniversePolymorphicIO.hs
|
182b6d6a8f
[ tests ] Move some compiler tests from Succeed to Compiler/simple.
|
пре 9 година |
|
UniversePolymorphicIO.options
|
c7083badc0
[ #5431 ] Added --ghc-strict.
|
пре 3 година |
|
UniversePolymorphicIO.out
|
86eb792a27
[ fix #2783 ] Most builtin modules may use postulates and still be safe
|
пре 5 година |
|
UnusedArguments.agda
|
666c99c3b0
Merge branch 'maint-2.4'
|
пре 8 година |
|
UnusedArguments.out
|
112e498b99
Merge branch 'stable-2.5'
|
пре 7 година |
|
VaryingClauseArity.agda
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
VaryingClauseArity.out
|
344d141e5f
[ tests ] Renamed exec-tests to compiler-tests
|
пре 9 година |
|
VecReverse.agda
|
c71681368f
[ fixed #5103 ] --allow-unsolved-metas in compilation
|
пре 4 година |
|
VecReverse.out
|
03c8272555
[ js ] Enable some more tests
|
пре 7 година |
|
VecReverseErased.agda
|
df563b2c57
[ compiler test ] cosmetics
|
пре 5 година |
|
VecReverseErased.out
|
f3919ebeba
[ #2757 ] first examples with @0 modality working
|
пре 6 година |
|
VecReverseIrr.agda
|
b5251f9511
[ #1602 ] Forgot to add one changed test file
|
пре 6 година |
|
VecReverseIrr.out
|
b190a2a417
[ treeless ] erase runtime irrelevant arguments (NonStrict relevance)
|
пре 8 година |
|
WfRec.agda
|
98f7d8dec9
[ fixed #1854 ] work-arounds for #1855 #1856 #1857 to get compiler-tests passing
|
пре 8 година |
|
WfRec.out
|
ebda4a2766
[ compiler test ] test that well-founded recursion compiles to efficient code
|
пре 9 година |
|
Word.agda
|
34436d634b
[ treeless ] test case for word64 comparison
|
пре 7 година |
|
Word.out
|
9fae511927
[ #4697 ] rename recCon-NOT-PRINTED to <record>.constructor
|
пре 4 година |
|
compiler-simple.agda-lib
|
def8152d2c
[ test ] added .agda-lib file to compiler/simple
|
пре 9 година |
|
uncons.agda
|
1eec63b1c5
[ re #4491 ] Add uncons primitive (#4494)
|
пре 4 година |
|
uncons.out
|
1eec63b1c5
[ re #4491 ] Add uncons primitive (#4494)
|
пре 4 година |
Nils Anders Danielsson