(* A (probably) minimal working example of Canonical Structures in Coq *)
Record Magma : Type :=
  Pack {
      sort : Type
    ; op : sort -> sort -> sort
    }.

Definition plus_magma : Magma := @Pack nat plus.
Definition mult_magma : Magma := @Pack nat mult.

Notation "x % y" := (@op _ x y) (at level 70).

Fail Check 5 % 4.

Canonical plus_magma.

Check 5 % 4.
Eval simpl in 5 % 4.