module InfixError; syntax infix 5 + ; axiom + : Type → Type → Type; axiom T : Type + Type + ; end;