Alex Weisberger (Mar 07 2022 at 00:18): Alex Weisberger (Mar 07 2022 at 00:18):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.
Maximilian Schaeffeler (Mar 08 2022 at 08:58):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 04 2025 at 01:44 UTC