From 10b56b90ad1e2674403fd17896c77c02993ca9fd Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 01:46:18 -0700 Subject: [PATCH] General.addErrorMessage, orErrorBindWithMessage --- src/General.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/General.v b/src/General.v index 457b421..3c82528 100644 --- a/src/General.v +++ b/src/General.v @@ -649,6 +649,18 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) := end. Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20). +Open Scope string_scope. +Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg := + match oe with + | Error s => Error (err_msg +++ eol +++ " " +++ s) + | OK t => f t + end. + +Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20). + +Definition addErrorMessage s {T} (x:OrError T) := + x >>=[ s ] (fun y => OK y). + Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type := | Indexed_Error : forall error_message:string, Indexed f (Error error_message) | Indexed_OK : forall t, f t -> Indexed f (OK t) -- 1.7.10.4