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.

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 it is a non-commutative Ring.

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)

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

Equations

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

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.

Equations

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