## Stream: general

### Topic: parser bug?

#### 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)

#### 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