## Stream: general

### Topic: macro paper

#### Sebastian Ullrich (Apr 01 2020 at 09:41):

I don't think it has been explicitly posted here before, so here is the IJCAR 2020 paper about Lean 4's macro system I wrote with @Leonardo de Moura: https://arxiv.org/abs/2001.10490
Feel free to ask questions or give feedback for the camera-ready version

#### Patrick Massot (Apr 01 2020 at 10:14):

You are right to post that message, although the paper appears on https://leanprover.github.io/publications/ and https://leanprover-community.github.io/links/. I have feedback: I implore you to stop using $\Rightarrow$ to mean $\mapsto$.

#### Johan Commelin (Apr 01 2020 at 10:34):

This is sweet!

macro "Σ" "(" idx:index ")" F:term : term =>(\big_ [HasAdd.add, 0] ($idx:index)$F)
-- end

-- We can already useΣwith the different kinds of index.
#check Σ (i <- [0, 2, 4] | i != 2) i
#check Σ (10≤i < 20 | i != 5) i+1
#check Σ (10≤i < 20) i+1

-- DefineΠ
macro "Π" "(" idx:index ")" F:term : term =>(\big_ [HasMul.mul, 1]($idx:index)$F)

-- The examples above now also work forΠ
#check Π (i <- [0, 2, 4] | i != 2) i
#check Π (10≤i < 20 | i != 5) i+1
#check Π (10≤i < 20) i+1


#### Patrick Massot (Apr 01 2020 at 10:40):

Yes, we can be grateful they didn't decide to use Σ for products and Π for sums!

#### Mario Carneiro (Apr 01 2020 at 10:43):

This doesn't cover all the lemmas and things like rw and simp applying in the right situations... notation isn't the only thing needed to make this set up work

#### Patrick Massot (Apr 01 2020 at 10:43):

This is a paper about macros, so it seems fair.

#### Mario Carneiro (Apr 01 2020 at 10:44):

that's true, I just want to remind folks that this isn't the main blocker for such notations in lean 3

Last updated: May 15 2021 at 02:11 UTC