Idris2-boot/tests/ttimp
Edwin Brady a59a104230 Implement 'rewrite' expressions
Mostly direct from Blodwen (some minor modifications to deal with new
way of going into a new scope in the elaborator as well as the usual
bits dealing with name lookup and Glued terms)
2019-05-27 12:15:37 +01:00
..
basic001 Added record declarations 2019-05-26 23:51:20 +01:00
basic002 Support eta in unification 2019-05-07 15:06:00 +01:00
basic003 Move some tests around 2019-05-26 11:34:02 +01:00
basic004 Initial implementation of 'case' blocks 2019-05-17 13:52:09 +01:00
basic005 Extend unification so that Functors work 2019-05-26 18:41:48 +01:00
basic006 Add test for failed delayed elaborator 2019-05-12 16:03:04 +01:00
dot001 Implement dot patterns 2019-05-25 18:39:21 +01:00
eta001 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
eta002 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
lazy001 Implement laziness 2019-05-22 19:42:43 +01:00
nest001 Implement local function definitions 2019-05-13 00:44:28 +01:00
nest002 Fix interaction between as patterns and case 2019-05-17 18:47:20 +01:00
perf001 Added record declarations 2019-05-26 23:51:20 +01:00
perf002 Let's not use exceptions for control flow... 2019-05-20 19:05:28 +01:00
perf003 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
qtt001 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
qtt002 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
qtt003 Check pattern variables don't unify with things 2019-05-25 20:18:43 +01:00
record001 Added record declarations 2019-05-26 23:51:20 +01:00
record002 Add (dependent) record update 2019-05-27 10:56:13 +01:00
rewrite001 Implement 'rewrite' expressions 2019-05-27 12:15:37 +01:00
search001 Move some tests around 2019-05-26 11:34:02 +01:00
search002 Move some tests around 2019-05-26 11:34:02 +01:00
search003 Improve auto search to support interfaces 2019-05-26 14:28:38 +01:00
search004 Extend unification so that Functors work 2019-05-26 18:41:48 +01:00