The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

On Thu, Nov 5, 2015 at 9:46 AM, Michael Shulman 
<shulman AT sandiego.edu>
 wrote:
>> I think you can hack with Unicode: the following seems to work for me,
>> where "␣" stands for a zero-width space (U+200B).
>>
>> Notation "f ␣( x )" := (f x)
>>   (at level 1, left associativity, format "f ␣( x )").
>
> Cute!  This does work, except that it still causes implicit arguments
> to be displayed:
>
> Definition idfunc {T:Type} (x:T) : T := x.
> Check (fun (T:Type) (x:T) => idfunc x = x).
> (* fun (T : Type) (x : T) => idfunc(T) x = x *)

Here's something that seems to work if I'm willing to box up the
functions that I want this notation to apply to (which is no problem):

Record func (A B : Type) := infunc { unfunc :> A -> B }.
Add Printing Coercion unfunc.
Notation "f ␣( x )" := (@unfunc _ _ f x)
  (at level 1, left associativity, format "f ␣( x )").

(Thanks, Hugo, in the other thread, for giving me the correct syntax
for "Add Printing Coercion"!)

Mike