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