Grind and Noncommutative rings?

Stream: lean4

[Siddharth Bhat]

I saw https://github.com/leanprover/lean4/pull/8343/, which prepares grind to work with noncommutative rings. I was wondering what decision procedures are planned to be implemented: I don't know of any "standard" decision procedure to decide the equational theory of noncommutative ring, and so would appreciate a pointer to the literature :)

[Kim Morrison]

No decision procedures, just normal forms.

[Kim Morrison]

i.e. just the scope of Mathlib's noncomm_ring.