Re: [isabelle] adhoc_overloading Monad_Syntax.bind
AFAIK the situation has not changed since August 2015:
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