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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.