Stream: Coq users

Topic: ✔ targeting specific part of a goal to simplify

Notification Bot (Aug 23 2023 at 06:16):

Nicolas Rinaudo has marked this topic as resolved.

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: Oct 13 2024 at 01:02 UTC