dot notation

Stream: general

[Yury G. Kudryashov]

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]

Is there any good way to fix this?

[Yury G. Kudryashov]

I mean, make h.add c in this example work.

[Sebastien Gouezel]

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]

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

[Alex J. Best]

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

[Johan Commelin]

set_option rtl true [/joking]

[Sebastien Gouezel]

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

[Gabriel Ebner]

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

[Sebastien Gouezel]

Done.

[Kenny Lau]

it isn't so hard to parse for me

[Kevin Buzzard]

Maybe you know python?

[Kenny Lau]

I do know Python

[Chris Hughes]

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