## Stream: general

### Topic: notation

#### Reid Barton (Feb 28 2018 at 15:41):

Does anyone have a suggestion for Lean-friendly notation corresponding to TeX $f_*$ and $f^*$?
(Meaning whatever you want them to mean, but for example, post- and pre-composition with the morphism $f$.)

#### Reid Barton (Feb 28 2018 at 15:42):

Apparently there are no Unicode subscript or superscript asterisk characters

#### Reid Barton (Feb 28 2018 at 16:17):

f^* works okay for $f^*$, but f_* isn't as nice because f_ parses as a single identifier, so it needs a space.

#### Andrew Ashworth (Feb 28 2018 at 17:04):

you could cheat and use ＿, which is not _

#### Sebastian Ullrich (Feb 28 2018 at 17:07):

Or use one of the up/down arrows

#### Kevin Buzzard (Feb 08 2020 at 15:47):

Any mathematician : "Let $R$ be a ring and let $A$ and $B$ be $R$-algebras. Then...". Lean: {R : Type*} [comm_ring R] {A : Type*} [comm_ring A] {B : Type*} [comm_ring B] [algebra R A] [algebra R B]. Can we somehow make this Lean code look less scary to mathematicians? Of course $R$ is a type, that's why it's called $R$. I wouldn't write "let $x$ be a ring", that would be madness!

#### Jason Rute (Feb 08 2020 at 16:14):

I'm not saying Lean should do this, but in Scala this thing with type classes comes up often and they have created a separate notation for it.
Assume Ring is a type class in Scala with a field add and that + knows to look at add in rings to implement addition. Then one can write the following verbose definition in Scala.

def double[R](x: R)(implicit ringOfR: Ring[R]) = x + x


Notice that in Scala [R] is a type parameter, (x:R) is a regular parameter, and (implicit ringOfR: Ring[R]) is an implicit parameter (very similar to Lean's type class parameters).

One can also instead use the following shorthand type class notation where we "treat" R as if it is an element of Ring:

def double[R: Rign](x: R) = x + x


Now, this notation might be less ambiguous in Scala than in Lean, since Scala treats type parameters and regular parameters differently with different notation (i.e. Scala is not dependently typed).

A similar issue exists with sets in Lean. (A type class is to Types as sets are to Props.) We can write the convenient notation

example (s : set ℕ) : ∀ a ∈ s, a = a := sorry


But if we apply intro twice we get the messy notation

example (s : set ℕ) (a : ℕ) (H : a ∈ s) : a = a := sorry


One could imagine an alternative notation where one writes

example (s : set ℕ) (a ∈ s) : a = a := sorry


I'm not claiming the Lean notation should change, but it is food for thought...

#### Rob Lewis (Feb 08 2020 at 16:25):

One could imagine an alternative notation where one writes

example (s : set ℕ) (a ∈ s) : a = a := sorry


This actually works exactly as you wrote it. I've never been sure if it's intentional or a "feature" enabled by the bounded quantifier syntax. Given that the a ∈ s hypothesis gets the default name H, I don't think it's something we should encourage in mathlib.

#### Mario Carneiro (Feb 08 2020 at 16:25):

Here's the relevant lean 3 issue: https://github.com/leanprover/lean/issues/1522

#### Mario Carneiro (Feb 08 2020 at 16:26):

which would have allowed us to write just [algebra R A] [algebra R B]

#### Reid Barton (Feb 08 2020 at 19:46):

Bundling helps somewhat, e.g., {R : CommRing} etc., though it's tricky in algebra since you typically have a lot of different levels of structure floating around

#### Johan Commelin (Feb 15 2021 at 12:45):

How does Lean decide whether it will use my local notation for pretty printing in the goal state?

#### Johan Commelin (Feb 15 2021 at 12:46):

I currently have

variables (C : system_of_complexes)

/-- C.d is the differential C c i ⟶ C c (i+1) for a system of complexes C. -/
def differential (c : ℝ≥0) (i j : ℤ) (hij : i + 1 = j) :
C c i ⟶ C c j :=
(C.obj \$ op c).d i ≫ congr_hom _ rfl hij

local notation d := differential _ _ _ _ (by int_magic)


#### Johan Commelin (Feb 15 2021 at 12:46):

Here int_magic is a custom tactic that shouldn't be relevant (maybe it is?!)

#### Johan Commelin (Feb 15 2021 at 12:47):

I can succesfully use d when entering statements, but Lean doesn't use d in the goal window.

#### Gabriel Ebner (Feb 15 2021 at 12:59):

The Lean 3 pretty-printer is not particularly clever, it tries to syntactically match the notation. In your case it looks for a by int_magic in the goal state.

#### Johan Commelin (Feb 15 2021 at 13:03):

Ok, so this will never work :sad:

#### Gabriel Ebner (Feb 15 2021 at 13:04):

You could use auto params.

#### Johan Commelin (Feb 15 2021 at 13:15):

Except that those don't play well with bundled functions...

#### Johan Commelin (Feb 15 2021 at 13:15):

Probably the best investment of my time is porting mathlib to Lean4

#### Johan Commelin (Feb 15 2021 at 13:16):

That will solve these issues in a more principled way :laughing:

Last updated: May 14 2021 at 02:15 UTC