theory StateMonad imports Main "HOL-Library.Monad_Syntax" begin section "State Monad with Exceptions"