Unused variable in set constructor

Stream: new members

[Lars Ericson]

If I say

import Mathlib
def TotalSet := { n: ℕ | True }

I get warning message

unused variable `n`
note: this linter can be disabled with `set_option linter.unusedVariables false`

If I change it to

import Mathlib

def TotalSet := { _: ℕ | True }

I get error message

unexpected syntax
  {_ : ℕ | True}

Is there a way to satisfy the linter without disabling it?

[Ruben Van de Velde]

Does _n work?

[Lars Ericson]

Yes, thanks.

import Mathlib
def TotalSet := { _n: ℕ | True }