419593 (17) [Avatar] Offline
#1
Listing 4.16 pattern match using the name items causes conflict ( DataStore.idr ).
Renaming items in addToData is required.

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newitem]
    addToData (item :: items') = item :: addToData items'