I'm running into a surprising behavior related to records. Consider the following 2 record definitions:
record unpaginated_state =
Data :: "int set"
Page :: int
record external_state =
Data :: "int set"
They both contain a field named Data
. When constructing a value of type unpaginated_state
via:
⦇ Data = {5}, Page = 0 ⦈
I get an error:
Error in record input: expecting field "Refine.unpaginated_state.Data" but got "Page"
If I change one of the field names, no error occurs, which is why it feels like the record definitions are clashing in some way.
I don't know much about records, but in this case you can just use the qualified name
⦇ unpaginated_state.Data = {5}, Page = 0 ⦈
The order of the record definitions seems to matter, if you swap them you can construct the unpaginated_state
without the qualifier. Now the creation of an external state
fails of course.
Last updated: Nov 11 2024 at 01:24 UTC