Variable eol : string.
Extract Constant eol => "'\n':[]".
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a}, a -> T a
+; bindM : forall {a}{b}, T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
(* the Error monad *)
Inductive OrError (T:Type) :=
rewrite e in v; apply OK; apply v.
apply (Error (error_message (length l) n)).
Defined.
+
+