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?

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