module InfixError; syntax fixity add := binary {assoc := none}; syntax operator + add; axiom + : Type → Type → Type; axiom T : Type + Type + ; end;