Stream: Beginner Questions

Topic: Undoing `dest / intro` declarations

view this post on Zulip Hanno Becker (May 03 2024 at 05:29):

Hi. What's the analogue of [simp del] for dest/intro declarations? Is there one at the outer syntax level, or does one need to drop to ML?

view this post on Zulip Kevin Kappelmann (May 03 2024 at 08:03):

[rule del]

view this post on Zulip Hanno Becker (May 03 2024 at 08:46):

Oh! I didn't know this works for intro[!] and elim[!] alike

Last updated: Nov 13 2025 at 08:29 UTC