git.iko.soy/Idris-dev
on 385dcbf help sign in
history oflibs/base/Data/Vect.idr
all commits
be7689bMake Vect follow the naming convention of ListDavid Christiansen fe1d470Totality checking now looks inside case directlyEdwin Brady 7c5819bAdd Data.Vect.ViewsEdwin Brady 05c0ebaDetail in docstring for zipWith on Vect and StreamDavid Raymond Christiansen e55fe2fBinder name changes in Elem/ThereEdwin Brady 9ecaccaAdd Uninhabited for Elem x []Edwin Brady 68c019aChange export qualifier keywordsEdwin Brady 4d0a065Change "class/instance" keywordsEdwin Brady b49893eRename isLengthEdwin Brady 319d143Remove obsolete reflected tacticMelvar Chen 6e49c84Add Ordering composition and use it for Ord (Vect n a)Melvar Chen 6b4c4d2Give Vect.findIndices & Co a more useful typeMelvar Chen 3f24facClean up various Data.Vect functionsMelvar Chen 50b5031Merge VectType into Vect to be more like other Data.*Melvar Chen 1b96024Add a couple of convenience functions in Data.VectEdwin Brady 43127b1Move Fin, Vect and So from prelude to baseEdwin Brady edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi f0ed9e9First renaming attemptAhmad Salim Al-Sibahi 505905dRemove some needless 'using' blocksEdwin Brady 8aa1c71Add a decision procedure for Data.Vect.ElemMelvar Chen 10ef56bMore docstringsDavid Raymond Christiansen 40924dcMoved libraries around, removed 'effects' flagEdwin Brady