git.iko.soy/Idris-dev
on b188fe1 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.idrTiny comment fix Erased.idrChange export qualifier keywords Fin.idrAdd 'restrict' in Fin HVect.idrMake arguments implicit in HVect.Shows IORef.idrtest basic021 type checks List.idrPurify Idris of "return" Mod2.idrDeprecate '%assert_total' Morphisms.idrData.Morphisms: add casts between morphisms where possible So.idrChange export qualifier keywords String.idrExtra check in parseInteger Vect.idrAdd the Vect version of dropElem.