Stream: Beginner Questions

Topic: ✔ why doesn't "auto simp add:" work in this proof?

view this post on Zulip Adam Dingle (Mar 28 2026 at 14:13):

Thanks for the helpful reply. It taught me 3 things that I didn't know before:

  1. how to use simp_trace_new (though it only works in jEdit and I'm mostly using VSCode, so really I have to use simp_trace instead)

  2. that "simp flip" can invert the direction of a rewrite rule

  3. that when I prove any identity involving an equality, it's best to state it in the direction that is best for rewriting

view this post on Zulip Notification Bot (Mar 28 2026 at 14:13):

Adam Dingle has marked this topic as resolved.

Last updated: Apr 14 2026 at 09:21 UTC