git.iko.soy/Idris-dev
on 7e43af7 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.idrChanged libs to new record syntax. Complex.idrFix addition and subtraction of Complex Float. Erased.idrChanged (<$>) to (<*>) Fin.idrImprove Fin error rewriter to remove "fromInteger" 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.idrInstance docs: add some instance docs to libs ZZ.idrAdded the Zero Constructor to Data.Sign