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