Idris2-boot/tests/idris2
Edwin Brady a130952928 Switch buffers back to scheme FFI
It's just easier to deal with the memory management! But we should do
something more flexible here later.
2020-05-17 22:49:41 +01:00
..
basic001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
basic002 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic003 Add prettyName 2020-03-18 19:33:19 +00:00
basic004 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic005 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
basic006 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic007 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic008 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic009 Better disambiguation of pairs 2020-03-31 18:12:34 +01:00
basic010 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
basic011 Add prettyName 2020-03-18 19:33:19 +00:00
basic012 Deal with non-existent files more gracefully 2019-07-07 13:10:14 +01:00
basic013 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic014 Add prettyName 2020-03-18 19:33:19 +00:00
basic015 Even more tests 2019-06-27 20:19:00 +01:00
basic016 Change argument unification order 2020-04-28 11:31:18 +01:00
basic017 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
basic018 Evaluate primitives (fromInteger etc) 2020-04-23 21:21:08 +01:00
basic019 Do another round of inlining, and io_bind 2020-05-12 11:33:29 +01:00
basic020 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic021 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic022 Add prettyName 2020-03-18 19:33:19 +00:00
basic023 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
basic024 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
basic025 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01: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 Merge remote-tracking branch 'upstream/master' into better-ide-mode 2019-12-08 13:09:08 +01:00
basic029 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
basic030 Update test output 2020-05-13 19:06:22 +01:00
basic031 Add prettyName 2020-03-18 19:33:19 +00:00
basic032 Add idiom brackets 2020-01-26 17:24:25 +00:00
basic033 Add prettyName 2020-03-18 19:33:19 +00:00
basic034 Add prettyName 2020-03-18 19:33:19 +00:00
basic035 Implement 'using' notation 2020-02-11 17:27:04 +00:00
basic036 Evaluate primitives (fromInteger etc) 2020-04-23 21:21:08 +01:00
basic037 [ fix #279 ] comment delimiters with more than one dash 2020-04-14 14:13:38 +01:00
basic038 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
basic039 Do compiling/inlining per module 2020-05-14 11:42:09 +01:00
basic040 [ test ] add test for defaulting peculiarity (#376) 2020-05-16 00:43:17 +01:00
coverage001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
coverage002 Better approach to erasure in pattern matching 2020-01-21 18:47:43 +00:00
coverage003 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
coverage004 Add prettyName 2020-03-18 19:33:19 +00:00
coverage005 Add missing test file 2020-02-23 22:20:11 +00:00
coverage006 Add coverage006 test 2020-03-18 14:39:59 +00:00
error001 Rabbit hole 2020-03-27 00:11:21 +00:00
error002 Rabbit hole 2020-03-27 00:11:21 +00:00
error003 Add prettyName 2020-03-18 19:33:19 +00:00
error004 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
error005 Add prettyName 2020-03-18 19:33:19 +00:00
error006 Change order of argument search in auto implicits 2020-04-10 15:39:45 +01:00
error007 Add prettyName 2020-03-18 19:33:19 +00:00
error008 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
error009 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
error010 Add prettyName 2020-03-18 19:33:19 +00:00
import001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
import002 Add prettyName 2020-03-18 19:33:19 +00:00
import003 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
import004 Print banner before typechecking 2019-10-26 13:39:50 +01:00
interactive001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
interactive002 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
interactive003 Merge remote-tracking branch 'upstream/master' into better-ide-mode 2019-12-08 13:09:08 +01:00
interactive004 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
interactive005 Tweak expression search heuristic 2020-02-15 23:24:00 +00:00
interactive006 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
interactive007 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
interactive008 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
interactive009 Rabbit hole 2020-03-27 00:11:21 +00:00
interactive010 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
interactive011 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
interactive012 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
interface001 Better disambiguation of pairs 2020-03-31 18:12:34 +01:00
interface002 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
interface003 Don't show MN names in hole contexts 2020-02-15 22:33:13 +00:00
interface004 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07: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 Auto implicit search fix 2019-10-18 18:26:32 +01:00
interface008 Add prettyName 2020-03-18 19:33:19 +00:00
interface009 Rabbit hole 2020-03-27 00:11:21 +00: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 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
interface013 Add prettyName 2020-03-18 19:33:19 +00:00
interface014 Push constraint name into default method impls 2019-09-20 19:01:07 +01:00
interface015 Add prettyName 2020-03-18 19:33:19 +00:00
interpreter001 Add test for Double subtraction 2019-12-22 21:50:18 +01:00
lazy001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
linear001 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
linear002 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
linear003 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
linear004 Further tweak to linearity rules 2019-12-29 15:21:08 +00:00
linear005 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
linear006 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
linear007 Add prettyName 2020-03-18 19:33:19 +00:00
linear008 Cut down default search depth 2020-02-13 18:23:40 +00:00
literate001 Enhance literate mode to recognise multi-modes. 2020-04-21 19:27:46 +01:00
literate002 Literate programming 2020-03-29 11:58:00 -07:00
literate003 Literate programming 2020-03-29 11:58:00 -07:00
literate004 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
literate005 Literate programming 2020-03-29 11:58:00 -07:00
literate006 Literate programming 2020-03-29 11:58:00 -07:00
literate007 Enhance literate mode to recognise multi-modes. 2020-04-21 19:27:46 +01:00
literate008 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
literate009 [ fix ] resugar to drop name prefixes 2020-04-03 20:00:59 +01:00
literate010 Enhance literate mode to recognise multi-modes. 2020-04-21 19:27:46 +01:00
literate011 Enhance literate mode to recognise multi-modes. 2020-04-21 19:27:46 +01:00
literate012 Update tests/idris2/literate012/expected 2020-04-22 20:37:07 +01:00
params001 Add prettyName 2020-03-18 19:33:19 +00:00
perf001 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
perf002 Remove unnecessary check from let elaboration 2019-07-31 10:10:47 +01:00
perf003 Add uniqueSearch data type option 2019-12-07 18:54:02 +00:00
perf004 Occasional performance boost 2020-04-12 18:01:45 +01:00
perror001 Check import hashes before a full parse 2020-02-10 15:47:19 +00:00
perror002 Parse primitive types as identifiers 2020-02-22 18:36:46 +00:00
perror003 Parse primitive types as identifiers 2020-02-22 18:36:46 +00:00
perror004 Check import hashes before a full parse 2020-02-10 15:47:19 +00:00
perror005 Parse primitive types as identifiers 2020-02-22 18:36:46 +00:00
perror006 Parse primitive types as identifiers 2020-02-22 18:36:46 +00:00
pkg001 Align the IPKG format more with the previous Idris implementation. 2019-08-01 12:47:08 +01:00
pkg002 Add --find-ipkg flag 2020-02-22 23:25:02 +00:00
real001 Unification tweak for getting lambda types 2020-02-09 17:05:22 +00:00
real002 Don't automatically apply implicits in let 2020-02-16 16:33:17 +00:00
record001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
record002 Adjust some tests. 2020-04-18 12:19:17 +02:00
record003 Rename record003 to record004. 2020-04-21 22:56:20 +02:00
record004 Add compatibility with the original record update syntax. 2020-04-27 18:02:25 +02:00
reg001 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
reg002 Change inference of function types in unification 2020-01-27 17:54:21 +00:00
reg003 Add prettyName 2020-03-18 19:33:19 +00:00
reg004 Disambiguate data constuctor families 2020-02-22 19:32:22 +00:00
reg005 Change argument unification order 2020-04-28 11:31:18 +01:00
reg006 Look under . for function name on lhs 2020-03-05 11:22:48 +00:00
reg007 Evaluate primitives (fromInteger etc) 2020-04-23 21:21:08 +01:00
reg008 Add --no-banner to test 2020-03-17 21:34:16 +00:00
reg009 Don't build run time case trees for Rig0 defs 2020-03-18 20:09:11 +00:00
reg010 Adjust some tests. 2020-04-18 12:19:17 +02:00
reg011 Elaborate record bodies on second mutual pass 2020-03-18 23:09:17 +00:00
reg012 Take account of env in record elaboration 2020-03-19 12:12:25 +00:00
reg013 Bugfix #269 2020-04-06 15:56:48 +01:00
reg014 Fix where under multiple cases 2020-04-09 18:47:39 +01:00
reg015 Allow flagging types as externally defined 2020-04-10 11:45:52 +01:00
reg016 update 'using' regression test 2020-04-22 16:53:02 -07:00
reg017 Fix lambda multiplicity check 2020-04-24 22:28:52 +01:00
reg018 Change argument unification order 2020-04-28 11:31:18 +01:00
reg019 Fix laziness bookkeeping in unification 2020-05-09 19:19:26 +01:00
total001 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
total002 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
total003 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
total004 More documentation refreshing 2020-02-25 22:18:02 +00:00
total005 More documentation refreshing 2020-02-25 22:18:02 +00:00
total006 Switch buffers back to scheme FFI 2020-05-17 22:49:41 +01:00
with001 Forgot to add test files! 2019-07-30 12:33:49 +01:00
with002 Change argument unification order 2020-04-28 11:31:18 +01:00