Re: [isabelle] Issues with locale interpretation
There is indeed functionality missing in locales: there are no means of
declaring and reusing morphisms in interpretations, so each parameter
needs to be dealt with manually in every interpretation. This creates
the desire of "bundling up" parameters, which I believe is not a good
thing as it reduces flexibility. As you say, this is not a logical but a
significant practical limitation.
I haven't understood what the parameters of the "unbundled" locale
"incidence_system" would have looked like. For unbundling them you would
have to have fixed sets of point and block parameters.
abbreviation “incidence_system’ X == incidence_system (points X)
interpretation add_point_in_sys: "incidence_system’ (add_point p)”
interpretation del_point_in_sys: "incidence_system’ (del_point p)”
This approach would require an abbreviation per locale, so it's probably
not as effective as dealing with morphisms directly.
This archive was generated by a fusion of
Pipermail (Mailman edition) and