Ring ids are assigned by Sym.Arith.classify?, which tries CommRing, Ring, CommSemiring, and Semiring in this order and caches the result for the whole run. The functions below select one class of the result; a type has at most one.

def Lean.Meta.Grind.Arith.CommRing.getCommRingId? (type : Expr) : GoalM (Option Nat)

Returns the ring id for the given type if there is a CommRing instance for it.

def Lean.Meta.Grind.Arith.CommRing.getNonCommRingId? (type : Expr) : GoalM (Option Nat)

Returns the ring id for the given type if it is a non-commutative Ring.

def Lean.Meta.Grind.Arith.CommRing.getCommSemiringId? (type : Expr) : GoalM (Option Nat)

Returns the semiring id for the given type if it is a CommSemiring (and not a CommRing).

def Lean.Meta.Grind.Arith.CommRing.getNonCommSemiringId? (type : Expr) : GoalM (Option Nat)

Returns the semiring id for the given type if it is a non-commutative Semiring.