The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

Is there any way to get Coq to display function applications using the
traditional mathematician's notation "f(x)", with parentheses around
the argument?  I would be satisfied with a solution that only applied
to functions with a particular domain and codomain.  Coq accepts this
notation, of course, since the parentheses just group the "x"
unnecessarily, but then it displays it as "f x" instead.  I've tried
wrapping both the function and the arguments in dummy inductive types
so that I could define a Notation for the application, but in both
cases I had to declare a Coercion to get the input notation to work,
and apparently the Coercion then overrides the Notation for display as
well.

Context: I'm using Coq to teach an introductory logic class for
mathematicians.  It would be nice if it used the same notation that
they'll see in their textbooks and everywhere else in mathematics.

Ironically, two-variable functions (or more) work fine, if I define
them uncurried (albeit with an extra space): the ordered pair (x,y)
always gets displayed with parentheses so that f applied to it looks
like "f (x,y)".  But I can't figure out any trick for one-variable
functions.

Mike