mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
4ae01d7264
The required totality of interface methods is now only affected if there's an explicit modifier on the method. This allows us to set %default total on the Prelude, which is a good thing to do anyway, without also requiring that every implementation of the interface in the prelude has to be total, which would potentially be a pain. Another good affect is that it speeds up totality checking elsewhere because totality checking is done lazily, and so with the total flag set we know in advance that prelude functions are total. |
||
|---|---|---|
| .. | ||
| Builtin.idr | ||
| Makefile | ||
| Prelude.idr | ||
| prelude.ipkg | ||
| PrimIO.idr | ||