git.iko.soy/Idris-dev
on cb80367 help sign in
Idris-dev/libs/contrib/Data
9 folders, 22 files
../ Bool/Text.Lexer: add `concat` Combinators/Added various combinators, most of which are also present in Haskell Fin/Elements of Fin when converted to Nat are smaller than the Bound. (#3407) List/Added export and totality directives (#4360) Matrix/Moved `abs` from the `Neg` interface into its own `Abs` interface. (Issue 3500) Nat/Changed the file name and location so this will build properly renamed: Data/Nat/Difference.idr -> Data/Nat.idr Pairs/add Data.Pairs.Implicit for converting erased pairs Stream/improve documentation for Data.Stream.Extra.startWith String/Data.String.Extra: more String utilities BoundedList.idrAdd conversions between BoundedList and Vect Chain.idrVarious additions to contrib (#4343) CoList.idrUpdate CoList.idr Combinators.idrVarious additions to contrib (#4343) Fuel.idrmove `Fuel` data type into its own module Fun.idrChange export qualifier keywords Graph.idrMove Graph.idr & Polyhedra.idr to contrib. Hash.idrChange export qualifier keywords Heap.idradd Uninhabited instances for True=False, remove unused proof from Data.Heap IOArray.idrAdded Data.IOArray for mutable array primitives Matrix.idrChange export qualifier keywords Monoid.idrStarted work on Data.Monoid Nat.idrChanged the file name and location so this will build properly renamed: Data/Nat/Difference.idr -> Data/Nat.idr Polyhedra.idrMove Graph.idr & Polyhedra.idr to contrib. PosNat.idrFixed `Data.SortedBag.contains` and added docs to Data.PosNat (#4348) Rel.idrChange export qualifier keywords Sign.idrextend Data.Sign SortedBag.idrFixed `Data.SortedBag.contains` and added docs to Data.PosNat (#4348) SortedMap.idrVarious additions to contrib (#4343) SortedSet.idrForgot a few `export`s Storable.idrPurify Idris of "return" ZZ.idrMoved `abs` from the `Neg` interface into its own `Abs` interface. (Issue 3500)