postfix constructors?

Stream: new members

[Thorsten Altenkirch]

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]

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]

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

[Kevin Buzzard]

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

[Shing Tak Lam]

Kevin Buzzard said:

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

local attribute [pp_nodot] nat.succ