홈 탐색 도움말
로그인
caryoscelus
/
agda
Watch 1
Star 0
포크 0
파일 이슈 0 풀 리퀘스트 0 위키
브렌치: js_amd_patch
브랜치 태그
agda
/
test
/
Compiler
/
simple
Nils Anders Danielsson b52a21df38 [ #5731 ] Added --save-metas and --no-save-metas. 2 년 전
..
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 년 전