git.iko.soy/Idris-dev
on 642efb3 help sign in
Idris-dev/libs/base/Data
1 folder, 23 files
../ Vect/Move Fin, Vect and So from prelude to base Bits.idrMove Fin, Vect and So from prelude to base BoundedList.idrMove Fin, Vect and So from prelude to base Buffer.idrMove Fin, Vect and So from prelude to base Complex.idrFix addition and subtraction of Complex Float. Erased.idrChanged (<$>) to (<*>) Fin.idrAdd missing file(!) Floats.idrRemove needless Prelude imports Fun.idrMove Fin, Vect and So from prelude to base HVect.idrMove Fin, Vect and So from prelude to base Hash.idrMove Fin, Vect and So from prelude to base Heap.idrRenamed VoidElim to void in order to ensure further consistency List.idrRemoved '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up Matrix.idrChanged (<$>) to (<*>) Mod2.idrUpdated inline comments to new style function documentation. Morphisms.idrChanged (<$>) to (<*>) Rel.idrUpdated inline comments to new style function documentation. Sign.idrAdded the Zero Constructor to Data.Sign So.idrMove Fin, Vect and So from prelude to base SortedMap.idrFixed bug regarding insertion in SortedMap. Fixes idris-lang/Idris-dev#1394. Solution based on the diagnosis in @sebzim4500s comment. SortedSet.idrAdd Foldable for SortedSet Vect.idrMove Fin, Vect and So from prelude to base VectType.idrChanged (<$>) to (<*>) ZZ.idrAdded the Zero Constructor to Data.Sign