`srw` should rewrite everywhere in goal by default, not just first occurrence

verse-lab / lean-ssr

LeanSSR: an SSReflect-Like Tactic Language for Lean

Apache License 2.0

31 stars 0 forks source link

`srw` should rewrite everywhere in goal by default, not just first occurrence #7

Open dranov opened 6 months ago

dranov commented 6 months ago

Maybe also print a helper message of how to rewrite a single occurrence if multiple are rewritten?

volodeyka commented 6 months ago

I strongly suspect this is the case only for unfolding. I don't know whether we should do something specific about that. Likewise, I remember specifying the exact location of unfold in ssreflect.coq quite frequently. Maybe let's use ?name for now?