def Lean.Meta.Grind.Arith.CommRing.isAddInst {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isAddInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getAddFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isMulInst {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isMulInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getMulFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isSubInst {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isSubInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getSubFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isNegInst {m : Type → Type} [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isNegInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getNegFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isPowInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isPowInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getPowFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isIntCastInst {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isIntCastInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getIntCastFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.isNatCastInst {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isNatCastInst inst = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getNatCastFn pure (Lean.Meta.Grind.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Grind.Arith.CommRing.reifyCore? {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadLiftT GoalM m] [MonadSetTermId m] (e : Expr) (skipVar : Bool) (gen : Nat) : m (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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.reify? e skipVar gen = Lean.Meta.Grind.Arith.CommRing.reifyCore? e skipVar gen

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

Equations

• Lean.Meta.Grind.Arith.CommRing.ncreify? e skipVar gen = Lean.Meta.Grind.Arith.CommRing.reifyCore? e skipVar gen

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

Similar to reify? but for CommSemiring

Equations

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