ITree.Events.Exception

Exception event

Throw exceptions of type Err.

Variant exceptE (Err : Type) : Type -> Type :=
| Throw : Err -> exceptE Err void.

Since the output type of Throw is void, we can make it an action with any return type.

Definition throw {Err : Type} {E F : Type -> Type} `{exceptE Err +? F -< E} {X}
           (e : Err)
  : itree E X
  := vis (Throw e) (fun v : void => match v with end).