Pretty-printing binary operations

Stream: mathlib4

[Yaël Dillies]

Can we make (·*·) pretty-print to (*) rather than the current (fun x x_1 ↦ x * x_1)?

[Scott Morrison]

Well, we would want it to pretty print back to (·*·).

[Yaël Dillies]

Am with anything that doesn't involve disambiguated auto-generated names!

[Scott Morrison]

Certainly we could hard code that for a few values of *. I'm not sure what criteria you would use generally.

[Yaël Dillies]

How does Lean 3 do it?

[Eric Wieser]

In lean 3, (*) is has_mul.mul

[Eric Wieser]

(·*·) is syntax for the version that isn't delta-reduced

[Yaël Dillies]

Do we want syntax for the delta-reduced version, then?

[Eric Wieser]

How does it currently print?

[Reid Barton]

Do you mean eta reduced?

[Eric Wieser]

I remember there's a page in some lean documentation that clearly lists what each name means, but I can never remember where to find it

[Mario Carneiro]

I've been thinking about that for a while - I expect that the fact that (.*.) isn't eta-reduced is going to bite us at some point since it is being recommended by mathport in places where lean 3 would have used (*) which is eta-reduced. The way I've been thinking of fixing the issue is to make (bla bla · bla ·) get converted to essentially eta_reduce_fun% x y => bla bla x bla ywhere eta_reduce_fun% is a macro which is like fun but eta reduces the resulting lambda if possible.

[Eric Wieser]

There are a small handful of cases where eta-reducing is undesirable, such as when working with finset.sum and wanting to rewrite under the binder; so I can see us potentially wanting a spelling for both the eta-reduced and non-reduced versions

[Mario Carneiro]

Assuming that the above is implemented, if you don't want to get it eta reduced you just shouldn't write it with the dot/paren notation. So fun x => foo x is not eta reduced but (foo .) is

[Mario Carneiro]

(foo . x) is of course not eta-reduced since it is not an eta redex

[Mario Carneiro]

As I see it, the lambdas were never really there in the source, and they are only being introduced as a desugaring. In the case of (.*.) we are clearly just using the syntax to be able to parse the infix operator * without adding much weirder things into the term grammar

[Mario Carneiro]

On that reading, we should be within our rights to not introduce the lambdas if we don't need them to express the function

[Kevin Buzzard]

Eric Wieser said:

I remember there's a page in some lean documentation that clearly lists what each name means, but I can never remember where to find it

It's here in the Lean 3 reference manual

[Eric Wieser]

Ah, my problem was that I was searching for the ascii spellings of the greek letters, not the letters themselves!