Stream: Coq users

Topic: ✔ targeting specific part of a goal to simplify


view this post on Zulip Notification Bot (Aug 23 2023 at 06:16):

Nicolas Rinaudo has marked this topic as resolved.

view this post on Zulip Nicolas Rinaudo (Aug 23 2023 at 06:33):

Thank you so much for this, it clarified things quite a bit!

It also makes me realise that you can do things with rewrite that I don't yet fully understand, but am slowly building an intuition for. It's a lot more suble than the blunt instrument I'm currently using it as (basically rewrite H or rewrite <- H, and sort of hope for the best).


Last updated: Jun 13 2024 at 19:02 UTC