Andre Dublin (4) [Avatar] Offline
#1
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