source
def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier (d : PolyDerivation) :
Int

Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`.

Equations

- d.getMultiplier = Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier.go✝ d 1

Instances For

source
structure Lean.Meta.Grind.Arith.CommRing.ProofM.State :
Type

- cache : Std.HashMap UInt64 Expr
- polyDecls : Std.HashMap Poly Expr
- monDecls : Std.HashMap Mon Expr
- exprDecls : Std.HashMap RingExpr Expr
- sexprDecls : Std.HashMap SemiringExpr Expr

Instances For

source
structure Lean.Meta.Grind.Arith.CommRing.ProofM.Context :
Type

- ctx : Expr
- sctx? : Option Expr

  Context for semiring variables if available

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.CommRing.ProofM (α : Type) :
Type
Equations

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

Instances For

source
partial def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toExprProof (c : EqCnstr) :
ProofM Expr
source
def Lean.Meta.Grind.Arith.CommRing.EqCnstr.setUnsat (c : EqCnstr) :
RingM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.setUnsat (c : DiseqCnstr) :
RingM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) :
RingM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) :
SemiringM Unit

Given `a` and `b`, such that `a ≠ b` in the core and `sa` and `sb` their reified semiring terms s.t. `sa.toPoly == sb.toPoly`, close the goal.

Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) :
NonCommRingM Unit

Given `a` and `b`, such that `a ≠ b` in the core and `ra` and `rb` their reified ring terms s.t. `ra.toPoly_nc == rb.toPoly_nc`, close the goal.

Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) :
NonCommSemiringM Unit

Given `a` and `b`, such that `a ≠ b` in the core and `sa` and `sb` their reified semiring terms s.t. `sa.toPolyS_nc == sb.toPolyS_nc`, close the goal.

Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) :
RingM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) :
RingM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) :
RingM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) :
NonCommRingM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) :
NonCommRingM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) :
NonCommRingM Expr
Equations

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

Instances For