*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] The theory Option*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 08 Oct 2014 13:21:59 +0200*In-reply-to*: <1DD2F112-6260-4A03-A42B-B1F33D94347C@scss.tcd.ie>*References*: <a06200713d059fe24adb2@[192.168.1.10]> <637E28C3-9D2A-4031-A0FD-D6887CCCC95E@in.tum.de> <1DD2F112-6260-4A03-A42B-B1F33D94347C@scss.tcd.ie>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2

Hallo, > I’m not sure what Isabelle/HOL theory introduces monads, but I am sure one exists. there is the Monad_Syntax theory (http://isabelle.in.tum.de/repos/isabelle/file/1329679abb2d/src/HOL/Library/Monad_Syntax.thy). However, this provides only syntax – Isabelle doesn't have a formalisation of the concept ‘monad’ in the way Haskell does. This would require parametrised typeclasses, which Isabelle doesn't have. It /does/ have specific monads, such as the option monad, the set monad, state monads, non-deterministic monads, etc. Even if you do use monads, you still have the problem that you have to state all of your lemmas in the form ’Just 1 + Just 1 = Just 2‘. Cheers, Manuel

**References**:**[isabelle] The theory Option***From:*W. Douglas Maurer

**Re: [isabelle] The theory Option***From:*Jasmin Christian Blanchette

**Re: [isabelle] The theory Option***From:*Andrew Butterfield

- Previous by Date: Re: [isabelle] The theory Option
- Next by Date: Re: [isabelle] The theory Option
- Previous by Thread: Re: [isabelle] The theory Option
- Next by Thread: Re: [isabelle] The theory Option
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list