# Zulip Chat Archive

## 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 `set`

s in Lean. (A type class is to `Type`

s as sets are to `Prop`

s.) 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: Aug 03 2023 at 10:10 UTC