Require Import Monad.
Require Import Exception.
Print throw.

Notation "'do' X <- T ; E" := (monad_bind _ T (fun X : _ => E)) (at level 0, X ident).

Notation " x <- f ; g " := (monad_bind (exM _) f (fun x => g)) (at level 50).
Notation " f ; g " := (monad_bind (exM _) f (fun _ => g)) (at level 52).
Notation " 'return' v " := (monad_return (exM _) v) (at level 52).

Notation " 'throw' v " := (throw _ v) (at level 40).
Notation " 'try' e 'with' x '=>' f " := (try_with e (fun x => f)) (at level 50).

Definition is_ok (n : nat) : ex nat bool :=
  try (match n with 0 => return true | _ => throw 1 end)
  with n => throw (S n).

Eval compute in (is_ok 1).