git.iko.soy/Idris-dev
on 735fbd2 help sign in
Idris-dev/libs/base/Data
5 folders, 12 files
../ List/Deal with bound variables in recoverableCoverage Nat/Added Data.String.Views Primitives/Deprecate '%assert_total' String/change export rules for module Vect/Add Data.Vect.Views Bits.idrDeprecate '%assert_total' Complex.idrTiny comment fix Erased.idrChange export qualifier keywords Fin.idrAdd 'restrict' in Fin HVect.idrMake arguments implicit in HVect.Shows List.idrPurify Idris of "return" Mod2.idrDeprecate '%assert_total' Morphisms.idrChange export qualifier keywords So.idrChange export qualifier keywords SortedSet.idrChange Instance to implementation (#3404) String.idrPurify Idris of "return" Vect.idrMake Vect follow the naming convention of List