git.iko.soy/Idris-dev
on 1c0bf46 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.idrAdd bitsToHexStr to Data.Bits Buffer.idrCorrect doc typos Complex.idrMoved `abs` from the `Neg` interface into its own `Abs` interface. (Issue 3500) Erased.idrChange export qualifier keywords Fin.idrFin.restrict fix (#4337) HVect.idrMake arguments implicit in HVect.Shows IORef.idrAdd minimal documentation List.idrImplement DecEq for Elem Mod2.idrDeprecate '%assert_total' Morphisms.idrData.Morphisms: add casts between morphisms where possible So.idrChange export qualifier keywords String.idrExtra check in parseInteger Vect.idrMinor cleanup