I don't think we want to do this; we're still holding out for an upstream fix that makes (· op ·) a elaborate as Op.op a, which is better than your new spelling. Another suggestion that was floated around was to add (*) as notation for unapplied HMul.hMul, etc.

cc @digama0, who had thoughts on a similar PR.

Surely if we can make (· op ·) elaborate as Op.op then we can make (a op ·) elaborate as Op.op a? We will eventually want this anyway as (a op ·) is more readable than (op) a (the left argument is on the right!).

And this is an improvement in the short term too, as can be evidenced by the number of dsimp I am removing.

Replacing (· * ·) with HMul.hMul is also an improvement (in terms of proof convenience) in the short term, but @digama0 did not like the idea of doing that. I guess really it depends if the plan is general eta reduction for · functions, or something special for binary operators.

I guess my point is that this PR is both a proof convenience and readability improvement in a way that other solutions will converge to if they improve both proof convenience and readability.

Replacing (· * ·) with HMul.hMul is also an improvement (in terms of proof convenience) in the short term, but @digama0 did not like the idea of doing that. I guess really it depends if the plan is general eta reduction for · functions, or something special for binary operators.

The implementation leanprover/lean4#2267 does general eta reduction, there is nothing specific to binary operators in it.

I support this PR, it is a mathportism (I really wanted to do this directly in mathport but there were some complications IIRC). If I or anyone else manages to figure out how to fix leanprover/lean4#2267 then both variants will come out the same.

It seems like you can find a few more with \(\(· ([^ ]+) ·\) ([\w(].*?)\), though you have to filter the results manually

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

I read through the 4k hits of ·.*· manually to see whether I'd missed any (spoiler: I had) and I've now also made sure I didn't add unnecessary brackets within a type ascription. Will check everything builds, then send it to bors.

bors merge

Merge conflict.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Check all files imported
• Build