git.iko.soy/Idris-dev
on fbd6471 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/Allow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings. Network/Remove "return" from Monad Prelude/Define Prelude.List.replicate in a way that doesn’t require %assert_total System/Remove "return" from Monad Builtins.idrDefault to Integer instead of Int, and adjust fromInteger accordingly IO.idrMake ChType a member of IntTy ITChar. 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