Bug in `ring_nf`?

Stream: mathlib4

[Heather Macbeth]

The following fails on current master, with x + 0 failing to be normalized to x:

import Mathlib.Tactic.Ring

example {x : ℕ} (hn : 0 < x) : 0 < x + 0 := by
  ring_nf -- does nothing
  with_reducible assumption

Any thoughts on what the bug might be?

[Mario Carneiro]

Yes, this was reported earlier

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring_nf.20failing.20to.20fully.20normalize

[Heather Macbeth]

Is it wontfix then?

[Mario Carneiro]

the fix requires some substantial new code

[Mario Carneiro]

for now there is !4#2171

[Heather Macbeth]

huh

hrmacbeth added this to Teaching Features last month

[Heather Macbeth]

I must have forgotten about this issue! Can I motivate anyone to add it to their to-do list? I expect to start to use ring_nf heavily in teaching in about two weeks.