Zulip Chat Archive
Stream: general
Topic: Bug in `ring_nf`?
Heather Macbeth (Jul 10 2022 at 01:48):
Is this expected behaviour of ring_nf?
import tactic.ring
variables {k m : ℤ}
example : k + (m + 2) = m + (k + 2) := by ring_nf -- fails
cc @Mario Carneiro
Mario Carneiro (Jul 10 2022 at 03:01):
looks like a bug
Last updated: Dec 20 2023 at 11:08 UTC