# Zulip Chat Archive

## Stream: general

### Topic: dot notation

#### Yury G. Kudryashov (May 23 2020 at 21:25):

I've tried to convert some lemmas about `eq_on_source`

in `local_equiv`

to use dot notation, and in many cases I can't use dot notation due to an issue illustrated by the following #mwe

```
def nat.same_parity (a b : ℕ) : Prop := a % 2 = b % 2
instance nat.same_parity_setoid : setoid ℕ :=
{ r := nat.same_parity,
iseqv := ⟨λ n, rfl, λ a b h, h.symm, λ a b c hab hbc, hab.trans hbc⟩}
axiom nat.same_parity.add {a b : ℕ} (h : a ≈ b) (c : ℕ) : a + c ≈ b + c
lemma nat.same_parity.add_one {a b : ℕ} (h : a ≈ b) : a + 1 ≈ b + 1 :=
nat.same_parity.add h 1 -- works
lemma nat.same_parity.add' {a b : ℕ} (h : a ≈ b) (c : ℕ) : a + c ≈ b + c :=
h.add c -- fails
lemma nat.same_parity.add_one' {a b : ℕ} (h : a ≈ b) : a + 1 ≈ b + 1 :=
h.add_one -- works
```

#### Yury G. Kudryashov (May 23 2020 at 21:26):

Is there any good way to fix this?

#### Yury G. Kudryashov (May 23 2020 at 21:26):

I mean, make `h.add c`

in this example work.

#### Sebastien Gouezel (May 30 2020 at 20:23):

Dot notation has become ubiquitous in the goal state recently, and this is in general very nice, but it is very hard to parse expressions such as

```
p * (x.log * (p - 1)).exp = (x.log * p).exp * (x⁻¹ * p)
```

Is there a trick to tell Lean that, for some functions, it should not use the dot notation?

#### Patrick Massot (May 30 2020 at 20:25):

Ouch, this is even worse than the `f.ker`

example.

#### Alex J. Best (May 30 2020 at 20:25):

#### Johan Commelin (May 30 2020 at 20:28):

`set_option rtl true`

[/joking]

#### Sebastien Gouezel (May 30 2020 at 20:30):

I want `@[please_dont_use_polish_notation] def exp := ...`

:)

#### Gabriel Ebner (May 30 2020 at 20:31):

Please file an issue so that we don't forget this.

#### Sebastien Gouezel (May 30 2020 at 20:36):

Done.

#### Kenny Lau (May 30 2020 at 20:37):

it isn't so hard to parse for me

#### Kevin Buzzard (May 30 2020 at 20:38):

Maybe you know python?

#### Kenny Lau (May 30 2020 at 20:39):

I do know Python

#### Chris Hughes (May 30 2020 at 20:47):

Could we have a rule like don't use dot notation if the namespace is already open?

Last updated: May 16 2021 at 21:11 UTC