Idris2-boot/tests/ttimp
Edwin Brady 6385cb6e0f A bit more on performance
Most notably, when elaborating deferring argument, if the hole
standing for the argument is still a hole, fill it in directly rather
than going via unification. This prevents some needless evaluation.
2019-05-20 18:41:08 +01:00
..
basic001 A bit more on performance 2019-05-20 18:41:08 +01:00
basic002 Support eta in unification 2019-05-07 15:06:00 +01:00
basic003 First attempt at linearity checking pass 2019-05-19 20:24:14 +01:00
basic004 Initial implementation of 'case' blocks 2019-05-17 13:52:09 +01:00
basic005 Give correct multiplicity count to arguments 2019-05-12 14:24:24 +01:00
basic006 Add test for failed delayed elaborator 2019-05-12 16:03:04 +01:00
basic007 First attempt at linearity checking pass 2019-05-19 20:24:14 +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
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 test framework (copied from Blodwen) 2019-05-07 10:43:02 +01:00
perf002 First attempt at linearity checking pass 2019-05-19 20:24:14 +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 Add a test for non linear LHS 2019-05-19 20:30:27 +01:00