implicit vs explicit

Stream: lean4

[Johan Commelin]

Lean 4 newbie question: is it possible to change whether an argument is implicit/explicit after a declaration has been made? I think this is possible in Coq, and I was wondering if Lean 4 supports this.
I think that there are pros and cons to such a feature, but I don't know how to weigh both sides.

[Mario Carneiro]

As far as I know, this is not possible without making an alias of the definition