Zulip Chat Archive
Stream: lean4
Topic: dunfold in lean4
Felipe (Dec 13 2022 at 21:01):
How are typeclass methods unfolded in tactic mode in lean4? It seems in lean3 dunfold would handle that. E.g., how to show that Nat.succ Nat.zero - 1 is just Nat.zero?
Last updated: Dec 20 2023 at 11:08 UTC