Re: [isabelle] adhoc_overloading Monad_Syntax.bind



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
>>
> 




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