Zulip Chat Archive

Stream: general

Topic: nth_rewrite can't rewrite inside of an implication

Artem Vasilev (May 17 2021 at 10:23):

The nth_rewrite tactic doesn't seem to find rewrite inside of an implication. Here is an example:

import tactic

example (n m k : ) (h : m = k) : n  m  n  m :=
  -- rw h, works, replaces both m's
  -- rw [h] {occs := occurrences.pos [1]}, works, replaces the first m
  -- nth_rewrite 0 h, fails, "not enough rewrites found"

Is this a bug? Should I create an issue on Github instead?

Scott Morrison (May 17 2021 at 10:42):

Interesting... want to try to fix it? :-) I wrote nth_rewrite, but I admit I'm not that keen on debugging it at the moment.

Yaël Dillies (May 17 2021 at 11:04):

I had the same problem with nth_rewrite_lhs/rhs

Last updated: Dec 20 2023 at 11:08 UTC