[isabelle] Abbreviations with adhoc-overloaded constants
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
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).
Some background context on my use case. I have a locale l for abstracting over a
monomorphic monad in some definition d. Later, I instantiate the monad operations in
different ways using locale import or interpretation. Unfortunately, I get huge terms
mentioning the global version l.d applied to all the instantiated locale parameters rather
than just <my chosen prefix>.d.
Thanks in advance for any hints,
This archive was generated by a fusion of
Pipermail (Mailman edition) and