## Stream: new members

### Topic: postfix constructors?

#### Thorsten Altenkirch (Sep 05 2020 at 13:19):

Now since I have reinstalled lean the goals look a bit weird:

 m.succ + n = m + n.succ


I don't think it looks like this before. Can I switch this back to prefix?

#### Kenny Lau (Sep 05 2020 at 13:23):

This is due to a recent (maybe 1 month old) update to Lean that uses projection notation by default (m : nat so nat.succ m becomes printed as m.succ). To switch it off, you can type set_option pp.structure_projections false before the theorem statement.

#### Kenny Lau (Sep 05 2020 at 13:23):

set_option pp.structure_projections false
lemma foo (m : ℕ) : nat.succ m = 0 :=
begin
end


#### Kevin Buzzard (Sep 05 2020 at 13:26):

Isn't there also a way of turning it off just for succ?

#### Shing Tak Lam (Sep 05 2020 at 14:00):

Kevin Buzzard said:

Isn't there also a way of turning it off just for succ?

local attribute [pp_nodot] nat.succ

Last updated: May 13 2021 at 23:16 UTC