Re: [isabelle] Abbreviations with adhoc-overloaded constants



Hi Florian,

On 06/08/15 11:16, Florian Haftmann wrote:
Hi Andreas,

Am 31.07.2015 um 12:16 schrieb Andreas Lochbihler:
Dear all,

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
interact smoothly.
You are probably right. If I disable adhoc-overloading for the uncheck phase using [[show_variants]], the abbreviations are contracted again.

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.

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.