mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-03 00:55:00 +03:00
9129df359f
If we're going to use assert_total. we might as well not have the distinction between empty and non empty results, which only makes the code harder to follow. Also there's some kind of issue which seems to mean the token list can't be erased if we do that. I will investigate if I can make a smaller example. |
||
|---|---|---|
| .. | ||
| Builtin.idr | ||
| Makefile | ||
| Prelude.idr | ||
| prelude.ipkg | ||
| PrimIO.idr | ||