git.iko.soy/Idris-dev
on 1b71663 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/Make covering function public export 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.idrnewBuffer should return a managed pointer Complex.idrEnabled Fractional instance for Complex a Erased.idrChange export qualifier keywords Fin.idrFin.restrict fix (#4337) HVect.idrMake arguments implicit in HVect.Shows IORef.idrThese are both called by Core.Core in Blodwen, which I also want to make %default total List.idrImplement DecEq for Elem Mod2.idrDeprecate '%assert_total' Morphisms.idrPrettify Monoids for morphisms So.idrChange export qualifier keywords String.idrExtra check in parseInteger Vect.idrAdd takeUpto and dropUpto functions to Data.Vect