coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit--Claudel <clement.pit AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] mathematical function notation
- Date: Tue, 3 Nov 2015 23:45:44 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
- Ironport-phdr: 9a23:KU+9nhz91y0782bXCy+O+j09IxM/srCxBDY+r6Qd0e4TIJqq85mqBkHD//Il1AaPBtWGragVwLWM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStOU1ZX8iLr60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWZg8O43YaTlIukwYNRiPB5Qz2U5O55iD+u+9w3jXcJczqZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==
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
- [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
- 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
- Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/05/2015
- Re: [Coq-Club] mathematical function notation, Cedric Auger, 11/04/2015
- Re: [Coq-Club] mathematical function notation, Michael Shulman, 11/04/2015
Archive powered by MHonArc 2.6.18.