edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-29 15:52:29 +03:00
Code Issues Projects Releases Wiki Activity
9bb91b5656
Idris2-boot/tests/idris2
History
Edwin Brady 9bb91b5656 Allow deferring definitions to other modules 
This is supported by Idris 1 and is handy for breaking cycles in
modules. To achieve this, we just need to make sure that complete
definitions aren't overwritten with empty definitions on loading.
2019-08-06 13:33:30 +01:00
..
basic001 Normalise holes in error messages 2019-06-30 17:23:19 +01:00
basic002 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
basic003 More tests moved over... 2019-06-25 21:50:48 +01:00
basic004 Set fresh name counter on loading Main ttc 2019-06-27 14:47:47 +01:00
basic005 Set fresh name counter on loading Main ttc 2019-06-27 14:47:47 +01:00
basic006 Set fresh name counter on loading Main ttc 2019-06-27 14:47:47 +01:00
basic007 Set fresh name counter on loading Main ttc 2019-06-27 14:47:47 +01:00
basic008 Set fresh name counter on loading Main ttc 2019-06-27 14:47:47 +01:00
basic009 More base libraries 2019-06-30 23:54:50 +01:00
basic010 Refine dot pattern rules 2019-06-27 19:16:33 +01:00
basic011 More tests from Blodwen 2019-06-27 19:33:02 +01:00
basic012 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
basic013 Even more tests 2019-06-27 20:19:00 +01:00
basic014 Even more tests 2019-06-27 20:19:00 +01:00
basic015 Even more tests 2019-06-27 20:19:00 +01:00
basic016 Add test for eta 2019-06-28 12:43:55 +01:00
basic017 Delay case elaboration 2019-07-02 16:53:41 +01:00
basic018 Add a couple more tests 2019-06-29 20:03:00 +01:00
basic019 Add a couple more tests 2019-06-29 20:03:00 +01:00
basic020 Fix loading of hints, and add test 2019-06-29 20:51:48 +01:00
basic021 Updating typecase, add tests 2019-06-29 21:32:19 +01:00
basic022 Updating typecase, add tests 2019-06-29 21:32:19 +01:00
basic023 Add parameters blocks 2019-06-29 23:55:17 +01:00
basic024 Desugar pattern matching lambdas 2019-07-03 15:11:57 +01:00
basic025 Numeric range syntax 2019-07-12 09:32:36 +02:00
basic026 Check under data constructor for holes 2019-07-20 21:09:33 +01:00
basic027 Bind auto implicit arg names in LHS 2019-07-26 16:58:02 +01:00
basic028 check noprelude option when starting up without loading a file #65 2019-07-30 13:56:27 +02:00
coverage001 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
coverage002 Fix coverage checker issue 2019-06-29 16:41:26 +01:00
coverage003 Adding missing test files 2019-07-09 09:22:50 +02:00
coverage004 Adding missing test files 2019-07-09 09:22:50 +02:00
error001 Normalise holes in error messages 2019-06-30 17:23:19 +01:00
error002 Add error message tests 2019-06-25 21:46:28 +01:00
error003 Add error message tests 2019-06-25 21:46:28 +01:00
error004 Add error message tests 2019-06-25 21:46:28 +01:00
error005 Add error message tests 2019-06-25 21:46:28 +01:00
error006 Add some Control.Monad things 2019-07-10 20:18:40 +02:00
error007 Unelaborate hole applications properly 2019-07-03 15:31:46 +01:00
error008 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
error009 Improve 'with' implementation 2019-07-08 12:55:55 +02:00
error010 Make sure hole names are unique 2019-07-28 21:04:55 +01:00
import001 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
import002 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
import003 Allow deferring definitions to other modules 2019-08-06 13:33:30 +01:00
interactive001 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
interactive002 Make sure hole names are unique 2019-07-28 21:04:55 +01:00
interactive003 Fix small error is as patterns 2019-06-24 15:30:36 +01:00
interactive004 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive005 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive006 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive007 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive008 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive009 More base libraries 2019-06-30 23:54:50 +01:00
interactive010 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive011 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interactive012 Finish adding interactive tests from Blodwen 2019-06-24 16:23:32 +01:00
interface001 Change equality elaboration 2019-07-05 11:26:45 +01:00
interface002 Place implicits through to method bodies 2019-07-20 16:25:40 +01:00
interface003 More interface tests 2019-06-24 18:04:43 +01:00
interface004 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
interface005 More interface tests 2019-06-24 18:04:43 +01:00
interface006 Add test for #25 2019-07-20 19:01:34 +01:00
interface007 Fix possible loop in auto implicit search 2019-07-22 11:21:34 +01:00
interface008 Allow marking interface methods multiplicities 2019-07-22 16:21:33 +01:00
interface009 Check for name clashes in impl constraints 2019-07-22 23:16:51 +01:00
interface010 Unbound implicits are invertible in terms 2019-07-26 12:27:54 +01:00
interface011 Add test for fix for #49 2019-07-26 23:13:11 +01:00
interface012 Update method names when checking default methods 2019-07-27 17:01:02 +01:00
interface013 Check implicit searches are complete 2019-07-28 18:27:43 +01:00
lazy001 Add a simple lazy Inf test 2019-06-24 18:08:32 +01:00
linear001 Add linearity tests 2019-06-27 19:28:14 +01:00
linear002 Add linearity tests 2019-06-27 19:28:14 +01:00
linear003 Add linearity tests 2019-06-27 19:28:14 +01:00
linear004 Add linearity tests 2019-06-27 19:28:14 +01:00
linear005 Add linearity tests 2019-06-27 19:28:14 +01:00
linear006 Allow annotating functions with multiplicity 2019-07-20 18:04:18 +01:00
linear007 Check under 'as' patterns for case arg usage 2019-07-20 18:57:03 +01:00
perf001 Change elaboration of lets 2019-07-28 13:43:01 +01:00
perf002 Remove unnecessary check from let elaboration 2019-07-31 10:10:47 +01:00
perror001 Add parse error tests from Blodwen 2019-06-29 21:37:30 +01:00
perror002 Add parse error tests from Blodwen 2019-06-29 21:37:30 +01:00
perror003 Add parse error tests from Blodwen 2019-06-29 21:37:30 +01:00
perror004 Add parse error tests from Blodwen 2019-06-29 21:37:30 +01:00
perror005 Add parse error tests from Blodwen 2019-06-29 21:37:30 +01:00
perror006 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
record001 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
record002 Add a couple of interactive tests 2019-06-24 15:16:49 +01:00
total001 Add first batch of totality checking tests 2019-06-24 18:14:07 +01:00
total002 Add first batch of totality checking tests 2019-06-24 18:14:07 +01:00
total003 Fix coverage checker issue 2019-06-29 16:41:26 +01:00
total004 Fix Total004 test 2019-07-06 15:55:47 +01:00
total005 Allow deferring definitions to other modules 2019-08-06 13:33:30 +01:00
total006 Add Range interface to prelude 2019-07-11 23:38:25 +02:00
with001 Forgot to add test files! 2019-07-30 12:33:49 +01:00