Zulip Chat Archive

Stream: general

Topic: parser bug?


view this post on Zulip Kevin Buzzard (Jun 25 2020 at 18:19):

Should

import tactic

example (P : Prop) : P  P := by {tauto!}

work? (it doesn't; but

example (P : Prop) : P  P := by {tauto! }

does)

view this post on Zulip Kenny Lau (Jun 25 2020 at 20:15):

well this doesn't matter because in the current style we always use { xxx } (one space after the opening bracket and one space before the closing bracket)


Last updated: May 13 2021 at 05:21 UTC