Algebra.BigOperators.Basic mathlib4#1628

Stream: mathlib4

[Johan Commelin]

Work started. PR is at mathlib4#1628.

[Johan Commelin]

Aahrg, immediately stuck on notation

[Johan Commelin]

I'm currently adding #align for all the additivized versions.

[Johan Commelin]

If someone can get the 4 notation lines at the top of the file working, that would be great.

[Johan Commelin]

-- mathport name: finset.sum_univ
-- scoped[BigOperators] -- Porting note: `notation3` doesn't mesh with `scoped[Foo]`
notation3"∑ "(...)", "r:(scoped f => Finset.sum Finset.univ f) => r

-- mathport name: finset.prod_univ
-- scoped[BigOperators] -- Porting note: `notation3` doesn't mesh with `scoped[Foo]`
notation3"∏ "(...)", "r:(scoped f => Finset.prod Finset.univ f) => r

-- mathport name: finset.sum
-- scoped[BigOperators] -- Porting note: `notation3` doesn't mesh with `scoped[Foo]`
notation3"∑ "(...)" in "s", "r:(scoped f => Finset.sum s f) => r

-- mathport name: finset.prod
-- scoped[BigOperators] -- Porting note: `notation3` doesn't mesh with `scoped[Foo]`
notation3"∏ "(...)" in "s", "r:(scoped f => Finset.prod s f) => r

works, for now

[Johan Commelin]

I'm stopping on this file for a bit

[Chris Hughes]

@Siddharth Bhat says he knows how to do it

[Chris Hughes]

@Siddharth Bhat has pushed

[Johan Commelin]

There also seems to be a bug in mathport which causes it to print literal "\n" strings in the docstring arguments to to_additive.

[Johan Commelin]

This file is now ~ 50% error free

[Johan Commelin]

I'm going to work on this file a bit more

[Johan Commelin]

I'm a bit concerned that none of the notation is showing in the goal view

[Johan Commelin]

CI is happy with this one

[Johan Commelin]

But notation is still not showing up in the goal view

[Siddharth Bhat]

Johan Commelin said:

But notation is still not showing up in the goal view

AFAIU, that's because I implemented it using macro_rules, which means I'd need to write a delaborator to show the notation. I shall check if it's possible to use higher level notation / macro that automatically generates the delaborator. If this is not possible, I shall implement the delaborator annotation.

[Johan Commelin]

Awesome, thanks!