mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-20 10:02:03 +03:00
40f72e74f0
* Case tree/coverage checking shortcuts We were calculating some things we didn't need - we can stop computing the type of a case operator when we know the head, because that's all we need for coverage checking. We can also abandon checking a left hand side for coverage purposes if we encounter an empty type. Both of these can save quite a bit of time in complex cases. * Normalisation heuristic for pattern variables If they get bit, fully normalise (like we do with case types) since it's likely a big term with lots of applications will normalise a lot. |
||
---|---|---|
.. | ||
Control | ||
Data | ||
Debug | ||
Decidable | ||
Language | ||
System | ||
base.ipkg | ||
Makefile | ||
System.idr |