Zulip Chat Archive

Stream: general

Topic: alias silently succeeds when name already exists


Floris van Doorn (Jul 24 2021 at 20:31):

@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 (Jul 24 2021 at 20:32):

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

Mario Carneiro (Jul 25 2021 at 06:20):

@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


Last updated: Dec 20 2023 at 11:08 UTC