Variable command bug?

Stream: lean4

[Marcus Rossel]

variable (a) (b)
variable {a b}

... causes:

failed to update variable binder annotation

Is this intended?

[Leonardo de Moura]

The second command was interpreted as a "binder annotation" update. However, the current implementation only supports this kind of update when the sequence of identifiers matches. That is, you can write

variable (a b)
variable {a b} -- Now 'a' and 'b' are implicit

or

variable (a) (b)
variable {a} {b} -- Now 'a' and 'b' are implicit

or

variable (a) (b)
variable {a}
variable {b}