noncomputable variable

Stream: general

[Mario Carneiro]

More random parser facts:

private noncomputable mutual variable x : ℕ -- not an error

In fact, the modifiers here are not unused; from the code it seems like the declaration modifiers will be propagated to nested definitions. I challenge anyone to find an example of a variable declaration that compiles differently depending on the modifiers

[Mario Carneiro]

apparently square bracket args aren't parsed like the other kinds:

variables [P Q : ℕ] -- parse error