Zulip Chat Archive
Stream: lean4
Topic: dedup
Jannis Limperg (Nov 16 2022 at 13:37):
Do we have something like mathlib3's docs#dedup yet?
Jannis Limperg (Nov 16 2022 at 16:02):
Ah, rename_i also renames shadowed hypotheses, so it can be used as a hygienic dedup. That's good enough for me.
Last updated: Dec 20 2023 at 11:08 UTC