Stream: new members
Christopher Hoskin (Mar 10 2021 at 20:41):
Sometimes I find myself trying to do something like
rw ← add_zero a to replace
a+0 in a goal. But I only want to do this for a particular occurrence of
a in the goal, whereas
rewrite replaces every occurrence. Is there a way to do this?
Bryan Gin-ge Chen (Mar 10 2021 at 20:43):
Christopher Hoskin (Mar 10 2021 at 20:45):
nth_rewrite is just what I was looking for.
Last updated: May 13 2021 at 20:13 UTC