edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 18:53:42 +03:00
Code Issues Projects Releases Wiki Activity
aaf07d52ce
Idris2-boot/tests/idris2
History
Edwin Brady ebafddcfc9 Look for scrutinee type in case 
We can work out what it should be since each case is supposed to have
the same type, so we can look ahead to the alternatives. This way, we
don't have to rely on the scrutinee alone to calculate the type of the
case block. (Idris 1 does this too but I've only just encountered the
need for it in Idris 2 now!)
2020-03-27 14:27:33 +00: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 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07: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 Add prettyName 2020-03-18 19:33:19 +00:00
basic017 Rabbit hole 2020-03-27 00:11:21 +00:00
basic018 Add prettyName 2020-03-18 19:33:19 +00:00
basic019 Add '--no-banner' option 2019-09-24 20:26:25 +06: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 Add '--no-banner' option 2019-09-24 20:26:25 +06:00
basic025 Add '--no-banner' option 2019-09-24 20:26:25 +06: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 Add multiple parameter block to test suite 2019-10-24 00:06:57 +03:00
basic030 Look for scrutinee type in case 2020-03-27 14:27:33 +00: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 Add default implicit arguments 2020-02-25 14:09:08 +00: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 Add prettyName 2020-03-18 19:33:19 +00: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 Add prettyName 2020-03-18 19:33:19 +00:00
error005 Add prettyName 2020-03-18 19:33:19 +00:00
error006 Add prettyName 2020-03-18 19:33:19 +00: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 make tests pass, tweaking repl's output 2019-10-31 07:14:46 +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 Rabbit hole 2020-03-27 00:11:21 +00: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 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07:00
interactive012 Update proof tutorial for Idris 2 2020-02-26 12:33:01 +00:00
interface001 Rabbit hole 2020-03-27 00:11:21 +00: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 Add prettyName 2020-03-18 19:33:19 +00: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
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
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 Remove trailing whitespace from Idris sources. 2019-10-25 14:24:25 -07: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 Add prettyName 2020-03-18 19:33:19 +00:00
reg006 Look under . for function name on lhs 2020-03-05 11:22:48 +00:00
reg007 Rabbit hole 2020-03-27 00:11:21 +00: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 Only record fields should be in a new namespace 2020-03-18 22:48:19 +00: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
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 More documentation refreshing 2020-02-25 22:18:02 +00:00
with001 Forgot to add test files! 2019-07-30 12:33:49 +01:00