def Lean.Meta.Grind.Arith.CommRing.isAddInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isMulInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isSubInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isNegInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isPowInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isIntCastInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.isNatCastInst (ring : Ring) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.CommRing.reify? (e : Expr) (skipVar : Bool := true) (gen : Nat := 0) : RingM (Option RingExpr)

Converts a Lean expression e in the CommRing into a CommRing.Expr object.

If skipVar is true, then the result is none if e is not an interpreted CommRing term. We use skipVar := false when processing inequalities, and skipVar := true for equalities and disequalities

partial def Lean.Meta.Grind.Arith.CommRing.reify?.go (toVar asVar : Expr → RingM RingExpr) (e : Expr) : RingM RingExpr

def Lean.Meta.Grind.Arith.CommRing.sreify? (e : Expr) : SemiringM (Option SemiringExpr)

Similar to reify? but for CommSemiring

partial def Lean.Meta.Grind.Arith.CommRing.sreify?.go (toVar asVar : Expr → SemiringM SemiringExpr) (e : Expr) : SemiringM SemiringExpr