Custom notation

Stream: general

[Martin Dvořák]

Here is some custom notation you might love or hate:
https://github.com/Ivan-Sergeyev/seymour/blob/cd2e76ca6adf338ee658fb75e7978df6dee06521/Seymour/Basic/Basic.lean#L3-L30

Feel free to copy without attribution.

[Eric Wieser]

/-- The left-to-right direction of `↔`. -/
postfix:max ".→" => Iff.mp

/-- The right-to-left direction of `↔`. -/
postfix:max ".←" => Iff.mpr

are kind of fun, though I think the first clashes with docs#PFun

[Eric Wieser]

Using "CANADIAN SYLLABICS R-CREE RE" (ᕃ) for insert seems rather out there

[Martin Dvořák]

Eric Wieser said:

/-- The left-to-right direction of `↔`. -/
postfix:max ".→" => Iff.mp

/-- The right-to-left direction of `↔`. -/
postfix:max ".←" => Iff.mpr

are kind of fun, though I think the first clashes with docs#PFun

Since it took me two years to realize what mp and mpr stands for (and I still sometimes don't know which one is which direction), it is pretty useful for me to have "arrow notation" on them.

[Martin Dvořák]

Eric Wieser said:

Using "CANADIAN SYLLABICS R-CREE RE" (ᕃ) for insert seems rather out there

Oooops! I thought it was non-alphabetical symbol.

[Eric Wieser]

Probably you should add |>.← notation with the right precedence too, to make it behave like other projections

[Martin Dvořák]

A few more custom notations I love:
https://github.com/Ivan-Sergeyev/seymour/blob/caf5948f250d71884fdbc8419029d43f766b33f0/Seymour/Basic/Basic.lean#L26

• prefix notation ↓ to mean fun _ =>
• postfix notation .≃ that converts Eq to Equiv
• infix notation ⊟ to mean Matrix.fromRows
• infix notation ◫ to mean Matrix.fromCols
• prefix notation ▬ to construct a single-row matrix from a vector (function)
• prefix notation ▮ to construct a single-column matrix from a vector (function)

The last two notations are especially useful for me because of the recent changes to the Matrix API.
Originally:
Matrix.row r
Then:
Matrix.row Unit r
Now:
Matrix.replicateRow Unit r
Things have been getting longer and longer to write but now I don't care because ▬r is all I write!

The downside is that you need a really good font to be able to read the code comfortably.

[Alok Singh]

Oh I love this thread, this could be a great meta one like the ambitious projects thread

[Alok Singh]

Martin Dvořák said:

A few more custom notations I love:
https://github.com/Ivan-Sergeyev/seymour/blob/caf5948f250d71884fdbc8419029d43f766b33f0/Seymour/Basic/Basic.lean#L26

• prefix notation ↓ to mean fun _ =>
• postfix notation .≃ that converts Eq to Equiv
• infix notation ⊟ to mean Matrix.fromRows
• infix notation ◫ to mean Matrix.fromCols
• prefix notation ▬ to construct a single-row matrix from a vector (function)
• prefix notation ▮ to construct a single-column matrix from a vector (function)

The last two notations are especially useful for me because of the recent changes to the Matrix API.
Originally:
Matrix.row r
Then:
Matrix.row Unit r
Now:
Matrix.replicateRow Unit r
Things have been getting longer and longer to write but now I don't care because ▬r is all I write!

The downside is that you need a really good font to be able to read the code comfortably.

what font do you use?

[Martin Dvořák]

Alok Singh said:

what font do you use?

JuliaMono, the same one doc-gen uses. My only complaint is that r looks a lil bit unusual in JuliaMono.

[Calvin Lee]

Martin Dvořák said:

My only complaint is that r looks a lil bit unusual in JuliaMono.

This is a toggleable opentype feature of JuliaMono: https://juliamono.netlify.app/#stylistic_sets (specifically ss10).

you can change these within vscode

[Ruben Van de Velde]

I was confused by your link because the font took quite long to load, so all the columns looked identical :sweat_smile:

[Martin Dvořák]

Calvin Lee said:

This is a toggleable opentype feature of JuliaMono: https://juliamono.netlify.app/#stylistic_sets (specifically ss10).

you can change these within vscode

Thanks!