[isabelle] adhoc_overloading Monad_Syntax.bind
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] adhoc_overloading Monad_Syntax.bind
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Fri, 12 Feb 2016 10:09:31 +0100
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.5.1
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
Thanks a lot for quick answers!
Description: S/MIME Cryptographic Signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and