conv giving metavariables

Stream: lean4

[Eric Rodriguez]

mwe:

example : ∀ p : Prop, p ↔ p := by
  conv => ext p; pattern p ↔ p; rw [iff_self]

/-
(kernel) declaration has metavariables '_example'

unsolved goals
⊢ ∀ (p : Prop), ?m.13 p -/

Is this a known issue? It seems to require both ext and pattern.

[Eric Wieser]

What's docs#pattern ?

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html

[Eric Rodriguez]

it's similar to conv in ... when it can be used

[Tomas Skrivan]

This bug definitely appeared on Zulip few times already(can't find it now) and I stumbled on it too. I never minimized it to such a small example. It would be nice to fill a github issue as there does not seem to be a one for this.

[Eric Rodriguez]

lean4#2877 for a github issue.

[Tomas Skrivan]

Thanks, just for later discoverability I would mention pattern in the title as the bug is in that tactic.