## 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 :=

lemma 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 :=


#### 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):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_matrix.20change/near/197841073

#### 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.

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?

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