Edwin Brady 04e4ebf80e Better approach to erasure in pattern matching ... It's a big patch, but the summary is that it's okay to use a pattern in an erased position if either: - the pattern can also be solved by unification (this is the same as 'dot patterns' for matching on non-constructor forms) - the argument position is detaggable w.r.t. non-erased arguments, which means we can tell which pattern it is without pattern matching The second case, in particular, means we can still pattern match on proof terms which turn out to be irrelevant, especially Refl. Fixes #178		2020-01-21 18:47:43 +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	Chapter 11 examples now working	2019-07-08 23:46:20 +02:00
coverage001	Chapter 11 examples now working	2019-07-08 23:46:20 +02:00
coverage002	Chapter 11 examples now working	2019-07-08 23:46:20 +02:00
dot001	Better approach to erasure in pattern matching	2020-01-21 18:47:43 +00:00
eta001	Make sure matches are not too specific	2019-06-29 19:28:04 +01:00
eta002	Chapter 11 examples now working	2019-07-08 23:46:20 +02: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	Delay case elaboration	2019-07-02 16:53:41 +01: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