coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coercions to Funclass and superfluous parentheses

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Coercions to Funclass and superfluous parentheses
Date: Fri, 12 Feb 2016 01:12:49 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:fOOiKx+NJzPUt/9uRHKM819IXTAuvvDOBiVQ1KB91e4cTK2v8tzYMVDF4r011RmSDdqdsK4P0rOO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU1Jj8jrnqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR/QMBzM/dmsx+cfDtB/ZTALJ6GFKAUsMlR8dOQ/P5hzgQt/SqCbwvOdnw2HOOMT3SbEyVjCj9LtwYAXvgi0KLSI66mzdgMFql+RdpETy9FRE34fIbdTNZ7JFdaTHcIZCSA==

Hi Coq Club,

In order to get nice notations for a deeply embedded functional language in Coq I tried to define application of my language as a coercion from trm to Fun_class. Although Coq is able to parse terms well, terms are not pretty printed back nicely. Superfluous parentheses are added, that make the pretty printed term pretty messy.

Does anyone know whether these parentheses can be avoided?

See below for some example code.

Best,

Robbert

==============

Parameter trm : Type.
Parameter app : trm -> trm -> trm.
Parameter u : trm.

Coercion app : trm >-> Funclass.

Check (u u). (* Prints "u u" *)
Check (u u u). (* Prints "(u u) u" *)
Check (u u u u). (* Prints "((u u) u) u" *)

[Coq-Club] Coercions to Funclass and superfluous parentheses, Robbert Krebbers, 02/12/2016