git.iko.soy/Idris-dev
on 413edee help sign in
Idris-dev/lib
8 folders, 8 files
../ Control/Remove "return" from Monad Data/Make additions public and require totality Debug/Add Debug.Trace Decidable/Add DecEq instances for list and tuple Language/Formatting improvements Network/Remove "return" from Monad Prelude/Integer literals for Fin If the elaborator can construct a proof that it is within bounds, integet literals can be used for Fins. Otherwise, a cryptic error message will be given. System/Remove "return" from Monad Builtins.idrDefault to Integer instead of Int, and adjust fromInteger accordingly IO.idrjavascript: make FFI work with HOFs MakefileRemove dynamically loaded RTS due to 32/64-bit issues on OS X Prelude.idrChange Show instance for Nat to show integers Providers.idrClean up implementation of type providers System.idrFriendly smart constructors for foreign integer types Uninhabited.idrAdded typeclass for uninhabited types base.ipkgAdd type-directed HVect functions and supporting Elem functions