git.iko.soy/Idris-dev
on cd87fcd 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/add 'public export' for all views and use 'really_believe_me' 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.idrMoved `abs` from the `Neg` interface into its own `Abs` interface. (Issue 3500) Erased.idrChange export qualifier keywords Fin.idrAdd 'restrict' in Fin HVect.idrMake arguments implicit in HVect.Shows IORef.idrtest basic021 type checks List.idrFixes #4161. Extracted mkNo to a top-level function for performance improvements Mod2.idrDeprecate '%assert_total' Morphisms.idrData.Morphisms: add casts between morphisms where possible So.idrChange export qualifier keywords String.idrExtra check in parseInteger Vect.idrAdds scanl1 to Data.Vect