Say I have a locale
A and a locale
B that imports it (extends it). When I interpret locale
A, I have to provide concrete parameters, which can be complex expressions. When I want to extend the interpretation to
B, I have to repeat these parameters it seems. How can I avoid that?
I think I could interpret
B together by technically just interpreting
B. However, my use case is actually more complex: It features a locale
C that upon interpretation automatically interprets
sublocale; so the “complex expressions” for the parameters of
A are provided once and for all, and I don’t want to write them again and again when interpreting
You mean definitions that repeat the parameters?
It always puzzled me that concrete locale parameters of interpretations aren’t accessible, when concrete instances of locale assumptions are, as is everything you define and proof within the locale context.
Ideally, I’d like to not have to write anything. Writing just underscores comes close, but this doesn’t do what I want (it tries to instantiate locale parameters with constants of the same names from the theory context, which usually is not what you want, I guess).
yeah but usually you want to have make the parameters opaque for the simplifier
it gets really annoying when simplifier decides that one of your parameters can be simplified (because they are always there, just hidden)
Last updated: Dec 07 2023 at 08:19 UTC