Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] mathematical function notation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] mathematical function notation


Chronological Thread 
  • 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: Wed, 4 Nov 2015 08:23:16 -0800
  • Authentication-results: mail2-smtp-roc.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-f177.google.com
  • Ironport-phdr: 9a23:tj71uxziCT2FN0vXCy+O+j09IxM/srCxBDY+r6Qd0ewXIJqq85mqBkHD//Il1AaPBtWGrakcwLqG+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStOU1Jz8h7D60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05w77vep01S3SBs3rSbU9X3z29Kd2TBrhjg8cPjg18WzYjYp9gL8N80HpnAB234OBONLdD/F5ZK6IJd4=
On Wed, Nov 4, 2015 at 8:00 AM, Michael Shulman
<shulman AT sandiego.edu>
wrote:
>> 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.
>
> This does work on its own. However, it also clobbers Coq's parsing
> for ever after.

Also, it apparently messes up the non-display of implicit arguments,
although I don't understand why:

Notation "f ( x )" := (f x) (at level 1, format "f ( x )").
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 *)

Somehow the implicit argument T of idfunc is getting displayed,
whereas the argument x is not getting parenthesized.

Archive powered by MHonArc 2.6.18.

Top of Page