instead of
items : (store : DataStore) -> Vect (size store) (schema store)
I think it should be
items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
due to the type in the DataStore being defined as
(items : Vect size (SchemaType schema))
in listing 5.6
|