Hugo Herbelin (Feb 04 2022 at 08:12): 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?
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
Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):for textual display modes, I guess trying to preserve parsability is a criteria
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
Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):Coq's choice of unified bindings is very interesting to me
Emilio Jesús Gallego Arias (Feb 04 2022 at 12:18):but poses this kind of questions
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: Oct 04 2023 at 19:01 UTC