Zulip Chat Archive
Stream: lean4
Topic: renameI can't handle composite names
Jakob von Raumer (Sep 13 2021 at 08:44):
renameI doesn't seem to recognize names as inaccessible, if they're composite:
example : (m n : Nat) → m = n := by
intro a.b a.b
renameI x
Leonardo de Moura (Sep 13 2021 at 13:45):
@Jakob von Raumer I pushed a fix for this. Now, renameI can rename shadowed names too.
Last updated: May 02 2025 at 03:31 UTC