Zulip Chat Archive

Stream: new members

Topic: dedup first occurrence


Bjørn Kjos-Hanssen (Oct 30 2022 at 18:04):

I have this:

u v: vector (fin b) t
u v: vector (fin 1) t

When I do dedup it changes the last occurrences of u, v to u_1, v_1. Is there a way to change the first occurrences instead?

Kevin Buzzard (Oct 30 2022 at 18:20):

Why do you even have that? Having different things with the same names is confusing.

Kevin Buzzard (Oct 30 2022 at 18:20):

Can you avoid having it?

Bjørn Kjos-Hanssen (Oct 30 2022 at 18:22):

I have a proof hb: b=1 so I did rw hb at u, rw hb at v

Ruben Van de Velde (Oct 30 2022 at 18:23):

What happens if you do subst hb instead?

Bjørn Kjos-Hanssen (Oct 30 2022 at 18:26):

Ah! That does it, thanks I didn't know about subst.


Last updated: Dec 20 2023 at 11:08 UTC