Re: [isabelle] adhoc_overloading Monad_Syntax.bind
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.
> So there's no way to reliably use adhoc_overlaoding with abbreviations.
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and