on 5e2000e help sign in
9 folders, 22 files
../ Bool/Text.Lexer: add `concat` Combinators/Added various combinators, most of which are also present in Haskell Fin/Proven some basic statements about Data.Fin. (#4571) 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.idrAdd `ltePlus` and `lteMult` to contrib. 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.idrAdd Show instance for SortedMap 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)