Zulip Chat Archive

Stream: new members

Topic: postfix constructors?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 05 2020 at 13:23):

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

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 13:26):

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

view this post on Zulip 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