Re: [isabelle] The theory Option



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




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