coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] mathematical function notation

From: Michael Shulman <shulman AT sandiego.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] mathematical function notation
Date: Thu, 5 Nov 2015 09:46:45 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f181.google.com
Ironport-phdr: 9a23:q+EhoRcadamZW7YdC78+2g4XlGMj4u6mDksu8pMizoh2WeGdxc68ZR7h7PlgxGXEQZ/co6odzbGG7ua7BCdcut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcaOKFkTzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePFyRrtBST8iLmod5cvxtBCFQxHFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63Xy/PMb2RL0wEQ+i8qNuQRmg3DwHKjo8+Wf/kcV2gKNWrxXnqhBild2HKLqJPeZzK/uONegRQnBMC55c

On Thu, Nov 5, 2015 at 1:49 AM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr>
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 *)

Can anything be done about that?

[Coq-Club] mathematical function notation, Michael Shulman, 11/04/2015
- Re: [Coq-Club] mathematical function notation, Clément Pit--Claudel, 11/04/2015
- Re: [Coq-Club] mathematical function notation, Cedric Auger, 11/04/2015
- Message not available
  - Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/04/2015
    - Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/04/2015
- Message not available
  - Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/04/2015
    - Re: [Coq-Club] mathematical function notation, Cedric Auger, 11/04/2015
      - Re: [Coq-Club] mathematical function notation, Pierre-Marie Pédrot, 11/05/2015
      - Message not available
        
        Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/05/2015
        
        Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/09/2015