Re: [isabelle] adhoc_overloading Monad_Syntax.bind



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


On 12/02/2016 10:30, Andreas Lochbihler wrote:
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

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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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