(* A specification monad *)
  Section SpecificationMonad.
    Definition SM (A : Type) : Type := @Datatypes.option (A * data (list operation)) .
    Definition SM_fail (A : Type) : SM A := None.
    Definition SM_return (A : Type) : (A * data (list operation)) -> SM A := Some.
    Definition SM_TODO (A : Type) : SM A := SM_fail A.
    Definition SM_bind {A B : Type} (m : SM A) (f : A -> SM B) : SM B :=
      match m with
      | Some (x, ops) =>
        match f x with
        | Some (y, ops') => Some (y, List.app ops ops')
        | None => None
        end
      | None => None
      end.
  End SpecificationMonad.


  Module Notations.
    (** Notation for the bind with a typed answer. *)
    Notation "'let!' x : A ':=' X 'in' Y" :=
      (SM_bind X (fun (x : A) => Y))
        (at level 200, x pattern, X at level 100, A at level 200, Y at level 200).

    (** Notation for the bind. *)
    Notation "'let!' x ':=' X 'in' Y" :=
      (SM_bind X (fun x => Y))
        (at level 200, x pattern, X at level 100, Y at level 200).

    Notation "X '&&>>' Y" :=
      (SM_bind X (fun _ => Y))
        (at level 100, Y at level 200).
  End Notations.
  Import Notations.