Set Implicit Arguments.
Unset Strict Implicit.

Section Exception_Type.

Inductive exc (V E : Set) : Set :=
  | Value : V -> exc V E
  | Error : E -> exc V E.

Variable V1 V2 E1 E2 : Set.

Definition excDecomp (C : Set) (e : exc V1 E1) (f : V1 -> C)
  (g : E1 -> C) : C := match e with
                       | Value x => f x
                       | Error y => g y
                       end.

Definition excValue (v : V1) : exc V1 E1 := Value E1 v.
Definition excRaise (b : E1) : exc V2 E1 := Error V2 b.

Definition excReraise (e : exc V1 E1) (f : V1 -> exc V2 E1) :
  exc V2 E1 := excDecomp e f (fun x => excRaise x).

End Exception_Type.


Notation "'try' id1 = e 'in' c 'with' id2 => d" :=
  (excDecomp e (fun id1 => c) (fun id2 => d))
  (at level 1, id1 ident, id2 ident, c, d, e at level 1).

Notation "'try' id1 = e 'in' c" := (excReraise e (fun id1 => c))
  (at level 1, id1 ident, c, e at level 1).

Notation "'try' id1 : T = e 'in' c" := (excReraise e (fun id1 : T => c))
  (at level 1, id1 ident, c, e at level 1, T at level 0).