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
|