Email Gateway (Aug 18 2022 at 18:56): Email Gateway (Aug 18 2022 at 18:56):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I have some locale that fixes quite a few parameters, as for example:
locale foo =
fixes a b c :: nat
begin
definition "const1 == a<c"
definition "const2 == a<c+b"
end
Now I want to interpret the locale, using some quite long
instantiations, eg:
interpretation prefix?: foo "(1+3)7" "(1+9)42" "91 - 11*2" .
All is nice up to here. However, when I start using the locale, e.g. in
lemma "const1 ==> const2"
then some horrible output occurs, that nobody want's to read any more:
foo.const1 ((1 + 3) * 7) (91 - 11 * 2) ==>
foo.const2 ((1 + 3) * 7) ((1 + 9) * 42) (91 - 11 * 2)
How can I change this behaviour, such that I get the plain names in the
output (or, if I used prefix!, the prefixed names).
Note: The locale tutorial sais that the current behaviour is the
intended one, but does not mention how
to change it.
Regards,
Peter
Email Gateway (Aug 18 2022 at 18:56):From: Clemens Ballarin <ballarin@in.tum.de>
You should be able to either introduce explicit abbreviations for your
constants in the global theory, or, if suitable concepts are already
available there, you might prefer to provide explicit mappings by
adding "where" clauses to your interpretation.
Clemens
Quoting Peter Lammich <lammich@in.tum.de>:
Last updated: Apr 26 2024 at 16:20 UTC