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

Question

以下代码：

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，但我不知道如何。

以下代码：类MonadState（M：类型->类型）（S：类型）：= MonadState_Build {monad_state：> Monad M;得到：M S;把：S-> M S; embed_fun {X} ：（​​ S-> ...

Answer 1

[没有内置库可用于处理monad。您需要定义自己的，或者找到一个并安装它。安装后，将其加载为Require Import。参见the section of the Coq manual on compiled files。