Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] adhoc_overloading Monad_Syntax.bind

view this post on Zulip Email Gateway (Aug 22 2022 at 12:36):

From: Tobias Nipkow <nipkow@in.tum.de>
I have problems combining adhoc_overloading Monad_Syntax.bind with
abbreviations. In the context of HOL-Probability:

adhoc_overloading Monad_Syntax.bind bind_pmf

abbreviation "f x y == (bind_pmf x (return_pmf o Pair y))"
term "f a b"

The output of the "term" command is the ugly rhs of the abbreviation (with infix

=). How can I phrase the abbreviation to make it work? Maybe with the help of
some translation?

Thanks a lot for quick answers!
Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tobias,

AFAIK the situation has not changed since August 2015:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-August/msg00031.html

So there's no way to reliably use adhoc_overlaoding with abbreviations.

Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Andreas,

On 02/12/2016 10:30 AM, Andreas Lochbihler wrote:

Hi Tobias,

AFAIK the situation has not changed since August 2015:

That is correct. The whole issue is on my radar, but after the last
attempt (together with Florian) to improve the situation I never really
came around to look at it again.

Anyway, the help of somebody who is more proficient in Isabelle
internals would be highly appreciated.

cheers

chris

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-August/msg00031.html

So there's no way to reliably use adhoc_overlaoding with abbreviations.

Andreas

On 12/02/16 10:09, Tobias Nipkow wrote:

I have problems combining adhoc_overloading Monad_Syntax.bind with
abbreviations. In the
context of HOL-Probability:

adhoc_overloading Monad_Syntax.bind bind_pmf

abbreviation "f x y == (bind_pmf x (return_pmf o Pair y))"
term "f a b"

The output of the "term" command is the ugly rhs of the abbreviation
(with infix >>=). How
can I phrase the abbreviation to make it work? Maybe with the help of
some translation?

Thanks a lot for quick answers!
Tobias

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Tobias Nipkow <nipkow@in.tum.de>
Thank you for the link. It mentions [[show_variants]] which would solve some of
my problems. Can that be used locally in a term antiquotation? This does not
work @{term [show_variants] ...}

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Makarius <makarius@sketis.net>
Try this:

setup ‹
Thy_Output.add_option @{binding show_variants}
(Config.put Adhoc_Overloading.show_variants o Thy_Output.boolean)›

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Makarius <makarius@sketis.net>
I have that also on my radar. Maybe we get a chance to discuss it together
soon.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:37):

From: Tobias Nipkow <nipkow@in.tum.de>
Cool, that helps!

Tobias
smime.p7s

Last updated: Apr 20 2024 at 01:05 UTC