alias silently succeeds when name already exists

Stream: general

[Floris van Doorn]

@Mario Carneiro is this intended? If you use alias and the declarations already exist, then alias does not raise an error.

import tactic.alias

alias iff.refl ↔ rfl eq.refl -- no error, but does nothing

[Floris van Doorn]

This came up in a PR where I added a new lemma, which broke a later alias command.

[Mario Carneiro]

@Floris van Doorn I don't really remember, and both possibilities seem acceptable to me. I can imagine that not erroring is sometimes helpful for autogenerated lemmas like in to_additive, but for explicit use erroring might help avoid typos. If you want to change it to give an error and fix any existing uses, be my guest