Zulip Chat Archive

Stream: general

Topic: macro paper


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 01 2020 at 10:40):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 01 2020 at 10:43):

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

view this post on Zulip 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