where to learn about writing notation

Stream: new members

[Patrick Lutz]

I don't know much about how to write notation in Lean. The two references I have looked at, Theorem Proving in Lean and the Lean Reference Manual, don't have that much to say on the topic. What's the best way to learn more?

To be more concrete, here's one thing I'd like to learn how to do. I've noticed that some notation in Lean allows for an arbitrary number of "arguments." For instance I can write {1, 2, 3, 4, 5, 6, 7, 8, 9} if I like and Lean knows that I mean a set with 9 elements. But the only way I know how to write notation in Lean, the number of arguments has to be fixed. How do I make notation that allows for a variable number of arguments?

[Alex J. Best]

I don't know any reference (which is not to say there isn't one) but I'd just search for the word notation in mathlib and look at the examples.
As for the {,,,} notation this is defined in core lean in c++ (https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp) and we can see what its really doing by turning notation off:

def t : set ℕ := {1,2,3}

set_option pp.notation false
#print t -- insert 1 (insert 2 (singleton 3))

so this although it looks like there are multiple arguments this is really just cleverly nesting inserts, so we can simulate this behaviour in our own notation (hacky version) with something like

notation `❰` a:1 := a
notation l `⸥ `:200 a:100 := insert l a
notation a`❱`:300 := singleton a
#check ❰1⸥ 2⸥ 3❱

[Reid Barton]

There's also the magic notation with foldr that you can find some examples of by searching for notation.*foldr

[Patrick Lutz]

Reid Barton said:

There's also the magic notation with foldr that you can find some examples of by searching for notation.*foldr

For some reason I can't figure out how to do this. When I try searching for this in the mathlib documentation online, I get a bunch of results that aren't actually notation, just other uses of foldr

[Patrick Lutz]

Although actually just searching for notation has turned up some examples using foldr

[Patrick Lutz]

It looks like those examples (e.g. data/matrix/notation) are very similar to the kind of thing I want to do