git.iko.soy/Idris-dev
on c6fe987 help sign in
Idris-dev/libs/base/Data
5 folders, 12 files
../ List/Deal with bound variables in recoverableCoverage Nat/Added Data.String.Views Primitives/Deprecate '%assert_total' String/change export rules for module Vect/Add Data.Vect.Views Bits.idrAdded docstrings for several public functions. Buffer.idrAdd Data.Buffer Complex.idrTiny comment fix Erased.idrChange export qualifier keywords Fin.idrAdd 'restrict' in Fin HVect.idrMake arguments implicit in HVect.Shows List.idrPurify Idris of "return" Mod2.idrDeprecate '%assert_total' Morphisms.idrChange export qualifier keywords So.idrChange export qualifier keywords String.idrExtra check in parseInteger Vect.idrMake Vect follow the naming convention of List