Re: [isabelle] Abbreviations with adhoc-overloaded constants
On 06/08/15 11:16, Florian Haftmann wrote:
You are probably right. If I disable adhoc-overloading for the uncheck phase using
[[show_variants]], the abbreviations are contracted again.
Am 31.07.2015 um 12:16 schrieb Andreas Lochbihler:
I am struggling with abbreviations that involve constants which have
been registered with adhoc_overloading. My problem is that I cannot get
Isabelle's pretty-printer to fold the abbreviations again.
Below is the minimal example (for Isabelle2015).
consts foo :: "'a â 'a"
consts foo_nat :: "nat â nat"
adhoc_overloading foo foo_nat
abbreviation bar :: "nat â nat" where "bar == id foo_nat" (* use
unoverloaded constant *)
term bar (* prints "id foo" *)
abbreviation bar' :: "nat â nat" where "bar' == id foo" (* use
overloaded constant *)
term bar' (* prints "id foo" *)
How can I make Isabelle's pretty printer contract the right-hand sides
of bar or bar' (all this should work also inside a locale).
this seems yet another instance of the fact that abbreviations, class
operations and adhoc-overloading in its current implementation do not
It requires substantial reforms here to get these more robust.
So for the time being, I have to decide between nice monad syntax and folded abbreviations.
This archive was generated by a fusion of
Pipermail (Mailman edition) and