git.iko.soy/Idris-dev
on 4bebb72 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/Type class resolution fix (disables Decidable.Decidable) Instances should not be resolved when there is no information available. Previously, resolution just guessed at an instance in this case, though this was never intended behaviour! 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