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.

This function will also perform sanity-checks (e.g., the Add instance for type must be definitionally equal to the CommRing.toAdd one.)

It also caches the functions representing +, *, -, ^, and intCast.

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

Returns the ring id for the given type if there is a Ring instance for it. This function is invoked only when getCommRingId? returns none.

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

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