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

Equations

• Lean.Meta.Grind.Arith.CommRing.isAddInst ring inst = Lean.Meta.Grind.isSameExpr ring.addFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isMulInst ring inst = Lean.Meta.Grind.isSameExpr ring.mulFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isSubInst ring inst = Lean.Meta.Grind.isSameExpr ring.subFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isNegInst ring inst = Lean.Meta.Grind.isSameExpr ring.negFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isPowInst ring inst = Lean.Meta.Grind.isSameExpr ring.powFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isIntCastInst ring inst = Lean.Meta.Grind.isSameExpr ring.intCastFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isNatCastInst ring inst = Lean.Meta.Grind.isSameExpr ring.natCastFn.appArg! inst

def Lean.Meta.Grind.Arith.CommRing.reify? (e : Expr) : RingM (Option RingExpr)

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

Equations

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

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