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.
+
+
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
- coreExprToWeakExpr e >>= fun e' =>
expectTyConApp te' nil >>= fun tca =>
- let (tc,lt) := tca in
+ let (tc,lt) := tca:(TyCon * list WeakType) in
((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
: ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match branches with