Zulip Chat Archive

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 Σ (10i < 20 | i != 5) i+1
#check Σ (10i < 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 Π (10i < 20 | i != 5) i+1
#check Π (10i < 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: Dec 20 2023 at 11:08 UTC