Zulip Chat Archive
Stream: new members
Topic: Vagaries of dsimp
Darij Grinberg (Oct 18 2025 at 18:36):
Why does this work:
intro x xnn y ynn
dsimp
intro hsq
but not this:
intro x xnn y ynn
intro hsq
dsimp at [hsq]
Darij Grinberg (Oct 18 2025 at 18:36):
(MiL section 4.2)
Aaron Liu (Oct 18 2025 at 19:27):
Should be dsimp at hsq, the spelling dsimp at [hsq] is a parse error
Darij Grinberg (Oct 18 2025 at 19:27):
oh facepalm
thank you!
Last updated: Dec 20 2025 at 21:32 UTC