projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
3b56536
)
General.addErrorMessage, orErrorBindWithMessage
author
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 14 Mar 2011 08:46:18 +0000
(
01:46
-0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 14 Mar 2011 08:46:18 +0000
(
01:46
-0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
457b421
..
3c82528
100644
(file)
--- 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).
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)
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)