rw bug priority of variables

Stream: lean4

[Jon Eugster]

Do we consider the following a bug? I would expect that the variable in context would take highest priority.

import Lean

open List

example (A B : Prop) (all : A ↔ B) (b : B) : A := by
  rw[all] -- error: failed to rewrite using equation theorems for 'List.all'
  assumption

[Alex J. Best]

Yes I think so

[Scott Morrison]

@Jon Eugster, could you open an issue? It would be good to note that simp succeeds here.

[Jon Eugster]

lean4#2729

[Scott Morrison]

If anyone would like to investigate this one that would be helpful. I'm happy to review the PR if there's an easy solution.

[Thomas Murrills]

Just to record it here: PR: lean4#2738