Wolfgang Jeltsch (Aug 02 2023 at 12:02): Wolfgang Jeltsch (Aug 02 2023 at 12:02):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 A and 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 A via 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 C.
Mathias Fleury (Aug 02 2023 at 13:05):create definitions?
Wolfgang Jeltsch (Aug 02 2023 at 13:32):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.
Wolfgang Jeltsch (Aug 02 2023 at 13:33):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).
Mathias Fleury (Aug 02 2023 at 13:54):yeah but usually you want to have make the parameters opaque for the simplifier
Mathias Fleury (Aug 02 2023 at 13:54):it gets really annoying when simplifier decides that one of your parameters can be simplified (because they are always there, just hidden)
Last updated: May 02 2024 at 08:19 UTC