The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Mike,

This works for me in 8.4pl4 and trunk:

    Notation "f ( x )" := (f x) (at level 1, format "f ( x )").

    Definition Linear f := forall x y, f(x + y) = f(x) + f(y).
    Print Linear.

    (* Linear = fun f : nat -> nat => forall x y : nat, f(x + y) = f(x) + 
f(y) *)
    (*      : (nat -> nat) -> Prop *)

(The format trick should also be useful to remove unwanted spaced in the 
multi-arguments case)

Clément.

On 11/03/2015 11:17 PM, Michael Shulman wrote:
> 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
>

Attachment: signature.asc
Description: OpenPGP digital signature