set vs. subtype

Stream: mathlib4

[Kenny Lau]

import Mathlib.Data.Set.Defs

variable (p : Nat → Prop)

-- {n | p n}
#check setOf fun n ↦ p n

-- { n // p n }
#check Subtype fun n ↦ p n

Note the spacing inconsistency: spaces inside brackets ({ n) for subtype, but not for set ({n)

[Kenny Lau]

image.png

this part

[Dan Velleman]

I think sets used to have those extra spaces, but they disappeared at some point.

[Kenny Lau]

@Dan Velleman this Lean 3 code from 8 years ago shows {x : nat | x > 0}

[Kenny Lau]

aha this lean 4 code 4 years ago shows the space

syntax "{ " ident " | " term " }" : term

[Kenny Lau]

here is the PR by Mario that changed it from space to no space, 2 years ago

[Kenny Lau]

here is the PR by Kevin Buzzard 4 years ago porting set to mathlib4, it has the space there

[Kenny Lau]

so perhaps Kevin introduced the spaces but Mario removed them to be consistent with Lean 3, but now that Set is entirely in mathlib (i.e. moved out of core), maybe we can put the spaces back?

[Dan Velleman]

I prefer it without the spaces.

[Kenny Lau]

@Dan Velleman @Michael Stoll does that apply to Subtype as well?