读取运算符>> =时Coq的语法错误

如下代码：

Class MonadState (M: Type -> Type) (S: Type) := MonadState_Build
    {
      monad_state :> Monad M;
      get : M S;
      put : S -> M S;
      embed_fun {X}: (S -> X) -> M X;
      run {X : Type} : M X -> S -> (X * S);
      embed_fun_assoc : forall X Y (f:S -> X) (g: X -> Y), embed_fun f >>= (fun x => ! g x) = embed_fun (compose g f);
      embed_fun_pure : forall X Y (f:S->X) (g: M Y), embed_fun f >> g = g;
      putget: forall (s: S), put s >> get = put s;
      putembed: forall X (s: S) (f: S->X), put s >> embed_fun f = put s >> ! f s;
      getput: forall f, get >>= (fun s => put (f s)) = embed_fun f >>= put;
      runput: forall s t, run (put s) t = (s, s);
      runbind: forall X Y (mx: M X) (my: X -> M Y) (s: S),
      run (mx >>= my) s = let (x, s') := run mx s in
      run (my x) s';
      runembed: forall X (f: S -> X) (s: S), run (embed_fun f) s = (f s, s);
    }.

给出以下错误：

Syntax error: [constr:operconstr] expected after '<' (in [constr:operconstr]).

我想我需要加载库才能与monad一起工作，但我不知道如何。