git.iko.soy/Idris-dev
on 4e326e4 help sign in
Idris-dev/libs/base/Data
5 folders, 13 files
../ List/mark covering functions using `sizeAccessible` as `public export total` so that they reduce in proofs Nat/mark covering functions using `sizeAccessible` as `public export total` so that they reduce in proofs Primitives/Deprecate '%assert_total' String/change export rules for module Vect/mark covering functions using `sizeAccessible` as `public export total` so that they reduce in proofs 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 IORef.idrAdded Data.IORef 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