pdf v 6

page 179
section 6.3.2

In the code example presented we have

schema : DataStore -> Schema
schema (MkData schema' size' items') = schema'

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData size' items') = items'

But it should be

schema : DataStore -> Schema
schema (MkData schema' size' items') = schema'

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData schema' size' items') = items'

Not terribly hard to figure out since it won't compile, and we are told the problem explicitly in the error