Zulip Chat Archive
Stream: general
Topic: rw buglet (I think)
Kevin Buzzard (Apr 02 2018 at 13:56):
before : 38 hypotheses including HyT2 : y ∈ T and HTUih : T = Ui h
Kevin Buzzard (Apr 02 2018 at 13:56):
Then I do rw HTUih at HyT2
Kevin Buzzard (Apr 02 2018 at 13:56):
and I end up with 39 hypotheses
Kenny Lau (Apr 02 2018 at 13:56):
quite hard to confirm it if you don't have MWE
Kenny Lau (Apr 02 2018 at 13:57):
oh that isn't a bug
Kenny Lau (Apr 02 2018 at 13:57):
because that hypothesis can't be replaced
Kevin Buzzard (Apr 02 2018 at 13:57):
including HyT2 : y ∈ T and HyT2 : y ∈ Ui h
Kenny Lau (Apr 02 2018 at 13:57):
because it's being used by other things
Kenny Lau (Apr 02 2018 at 13:57):
so instead it creates another hypothesis
Kevin Buzzard (Apr 02 2018 at 13:57):
Oh I see...
Kevin Buzzard (Apr 02 2018 at 13:58):
...with the same name?
Kenny Lau (Apr 02 2018 at 13:58):
well what other name would it be
Kenny Lau (Apr 02 2018 at 13:58):
you can do dedup if you don't like it
Kevin Buzzard (Apr 02 2018 at 13:58):
revert HyT2,intro HyT
Kevin Buzzard (Apr 02 2018 at 13:59):
It could have called it a ;-)
Last updated: Dec 20 2023 at 11:08 UTC