def Lean.Meta.Grind.Arith.CommRing.denoteNumCore (u : Level) (type semiringInst negFn : Expr) (k : Int) : Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getRingId? (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.getRingId?.go? (type : Expr) : GoalM (Option Nat)

Equations

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

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

Equations

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

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

Equations

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