Zulip Chat Archive
Stream: mathlib4
Topic: Dealing with `HMul` (etc.)?
Thomas Murrills (Dec 17 2022 at 00:22):
How do you unfold expressions like HMul.hMul all the way during a tactic? unfold doesn't seem to keep unfolding, and stops after one step.
(Or, should you try to avoid doing this?)
Thomas Murrills (Dec 17 2022 at 00:28):
(Turns out I could avoid this, but I'm still curious!)
Kevin Buzzard (Dec 17 2022 at 00:45):
Try delta?
Last updated: Dec 20 2023 at 11:08 UTC