Stream: Coq users

Topic: RFC: how to display fun/forall sequences mixed with let's


view this post on Zulip Hugo Herbelin (Feb 04 2022 at 08:12):

Hi, I have a design question regarding the term printer. When assumptions and local definitions are interleaved, as in

fun (x:nat) (y:=x+x) (z:nat) => x + z + y

or

forall (x:nat) (y:=x+x) (z:nat), x + z = y

that is, equivalently,

fun x:nat => let y := x+x in fun z:nat => x + z + y

and

forall x:nat => let y := x+x in forall z:nat, x + z = y

do we expect them (in general) to be printed in the "context" form (first syntax) or with the let explicitly separated (second syntax)?

Or would it depend on the length of the sequence of binders? Or depend of other criteria?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 12:17):

That's a very good question @Hugo Herbelin , in richer display models I'd expect the final rendering to be picked by the layout engine

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):

for textual display modes, I guess trying to preserve parsability is a criteria

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):

for those choices that are re-parsable, I dunno, seems to me like a matter of aestethics

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):

Coq's choice of unified bindings is very interesting to me

view this post on Zulip Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):

but poses this kind of questions

view this post on Zulip Hugo Herbelin (Feb 04 2022 at 12:29):

Yes, it is a question of aesthetics, and at some time also, at least when used with the idea of Context, of convenience and readibility, especially for big contexts. Maybe better not to change the current settings though, i.e. with an explicit let, as this is probably more mainstream and easier to understand at first.


Last updated: Feb 08 2023 at 23:03 UTC