mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 05:32:03 +03:00
819c9d7af1
At least as long as the number is small enough (currently set to < 100). This is because it can open up further evaluation opportunities when typechecking, and can make the term we're working with smaller - it also makes display a bit neater. Overall this makes some pathological cases of terrible performance much better, without hurting anything else. |
||
|---|---|---|
| .. | ||
| expected | ||
| Fin.idr | ||
| run | ||