git.iko.soy/Idris-dev
on aa42f71 help sign in
Idris-dev/lib/Prelude
15 files
../ Algebra.idruppercase modulenames Applicative.idrMake traverse_ total Cast.idrExpand integer primitive unification to encompass bigints Chars.idrAdd isNL/lines Complex.idrAdd Fin.strengthen Either.idrAdded typeclass for decidable equality plus instances for commonly-used datatypes Fin.idrInteger 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. Functor.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion Heap.idrChanged approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration. List.idrDefine Prelude.List.replicate in a way that doesn’t require %assert_total Maybe.idrRemove the unicode from the source files. Monad.idrRemove "return" from Monad Nat.idrDefault to Integer instead of Int, and adjust fromInteger accordingly Strings.idrDefault to Integer instead of Int, and adjust fromInteger accordingly Vect.idradd Data.HVect