Re: [isabelle] The theory Option


> I’m not sure what Isabelle/HOL theory introduces monads, but I am sure one exists.
there is the Monad_Syntax theory

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


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