macro paper

Stream: general

[Sebastian Ullrich]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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