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
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
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?
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
for textual display modes, I guess trying to preserve parsability is a criteria
for those choices that are re-parsable, I dunno, seems to me like a matter of aestethics
Coq's choice of unified bindings is very interesting to me
but poses this kind of questions
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