Email Gateway (Aug 19 2022 at 08:32): Email Gateway (Aug 19 2022 at 08:32):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I have a problem/question how abbreviations in locales are handled.
Regard the following toy example:
locale foo =
fixes a :: 'a
begin
abbreviation "f == (a,a,a)"
end
locale bar1 = s1!: foo a for a
begin
term "s1.f" -- printed as s1.f
end
locale bar2 = s1!: foo b for b
begin
term "s1.f" -- printed as (b,b,b)
end
Why is the abbreviation in the second case valid input syntax, but not
pretty-printed in output? And how can I change this behaviour, towards
also using the abbreviation in the output?
A similar problem arises when interpreting the locales.
After interpretation bar2 c (for constant c), the abbreviation "s1.f"
only works as input.
The current behaviour is somewhat strange, as it depends on the
conincidence of the parameter name in the locale expression
"s1!: foo a for a" and the fixed variable name "a" that was used when
declaring the locale.
In my concrete example, I use quite a lot of abbreviations, and one gets
easily confused if one always sees them expanded in the output. Concrete
example: "s1.lookup" vs. "map_op_lookup ops1"
Thanks in advance for any help/hints
Peter
Last updated: Nov 21 2024 at 12:39 UTC