mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-20 11:21:43 +03:00
4860d2b751
This is part of what we used to have in Enum but I think it's better to separate the two. Added implementations for Nat, and anything in Integral/Ord/Neg, so that we get range syntax (at least when its implemeted) for the most useful cases. |
||
---|---|---|
.. | ||
Builtin.idr | ||
Makefile | ||
Prelude.idr | ||
prelude.ipkg | ||
PrimIO.idr |