mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +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. |
||
---|---|---|
.. | ||
Reflection | ||
Reflection.idr |