Idris2-boot/tests/ttimp
Edwin Brady 722131f7d0 Simpler implementation of 'case'
Now only abstracts over the environment once and deals with 'where'
clauses by rewriting the nested name with the rearranged environment. As
a result, it interacts far better with local definitions (i.e. where
blocks).
2020-02-09 13:46:58 +00:00
..
basic001 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
basic002 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
basic003 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
basic004 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
basic005 Block reduction of private/export names 2019-06-15 16:10:01 +01:00
basic006 Bitwise operators 2020-01-31 16:25:19 +00:00
coverage001 Bitwise operators 2020-01-31 16:25:19 +00:00
coverage002 Bitwise operators 2020-01-31 16:25:19 +00:00
dot001 Bitwise operators 2020-01-31 16:25:19 +00:00
eta001 Make sure matches are not too specific 2019-06-29 19:28:04 +01:00
eta002 Bitwise operators 2020-01-31 16:25:19 +00:00
lazy001 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
nest001 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
nest002 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
perf001 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
perf002 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
perf003 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
qtt001 Add error message tests 2019-06-25 21:46:28 +01:00
qtt002 Simpler implementation of 'case' 2020-02-09 13:46:58 +00:00
qtt003 Check names are visible/public 2019-06-24 00:12:58 +01:00
record001 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
record002 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
rewrite001 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
search001 Name choice of holes 2020-01-11 22:52:18 +00:00
search002 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
search003 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
search004 Put built ttcs in build/ttc, rather than build 2019-09-04 12:41:16 +01:00
search005 Make sure matches are not too specific 2019-06-29 19:28:04 +01:00
total001 Change main program to be Idris2 2019-06-09 11:58:29 +01:00
total002 Fix some totality issues, add tests 2019-06-25 00:42:52 +01:00
total003 Allow deferring definitions to other modules 2019-08-06 13:33:30 +01:00
with001 Make sure matches are not too specific 2019-06-29 19:28:04 +01:00
with002 allow matching constants in with clauses fix #122 2019-10-15 21:52:44 +02:00