def Lean.Meta.Grind.Arith.Linear.get' : GoalM State

@[inline]

def Lean.Meta.Grind.Arith.Linear.modify' (f : State → State) : GoalM Unit

structure Lean.Meta.Grind.Arith.Linear.LinearM.Context : Type

• structId : Nat

class Lean.Meta.Grind.Arith.Linear.MonadGetStruct (m : Type → Type) : Type

• getStruct : m Struct

@[always_inline]

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] : MonadGetStruct n

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.LinearM (α : Type) : Type

We don't want to keep carrying the StructId around.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.LinearM.run {α : Type} (structId : Nat) (x : LinearM α) : GoalM α

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.getStructId : LinearM Nat

def Lean.Meta.Grind.Arith.Linear.LinearM.getStruct : LinearM Struct

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM : MonadGetStruct LinearM

def Lean.Meta.Grind.Arith.Linear.getRingCore? (ringId? : Option Nat) : GoalM (Option CommRing.Ring)

def Lean.Meta.Grind.Arith.Linear.throwNotRing {α : Type} : LinearM α

def Lean.Meta.Grind.Arith.Linear.throwNotCommRing {α : Type} : LinearM α

def Lean.Meta.Grind.Arith.Linear.getRing? : LinearM (Option CommRing.Ring)

def Lean.Meta.Grind.Arith.Linear.getRing : LinearM CommRing.Ring

instance Lean.Meta.Grind.Arith.Linear.instMonadGetRingLinearM : CommRing.MonadGetRing LinearM

def Lean.Meta.Grind.Arith.Linear.getZero : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getOne : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.withRingM {α : Type} (x : CommRing.RingM α) : LinearM α

def Lean.Meta.Grind.Arith.Linear.isCommRing : LinearM Bool

def Lean.Meta.Grind.Arith.Linear.isOrderedCommRing : LinearM Bool

def Lean.Meta.Grind.Arith.Linear.isLinearOrder : LinearM Bool

def Lean.Meta.Grind.Arith.Linear.hasNoNatZeroDivisors : LinearM Bool

@[inline]

def Lean.Meta.Grind.Arith.Linear.modifyStruct (f : Struct → Struct) : LinearM Unit

def Lean.Meta.Grind.Arith.Linear.getTermStructId? (e : Expr) : GoalM (Option Nat)

def Lean.Meta.Grind.Arith.Linear.setTermStructId (e : Expr) : LinearM Unit

def Lean.Meta.Grind.Arith.Linear.getNoNatDivInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getPreorderInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getOrderedAddInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.isOrderedAdd : LinearM Bool

def Lean.Meta.Grind.Arith.Linear.getLtFn {m : Type → Type} [Monad m] [MonadError m] [MonadGetStruct m] : m Expr

def Lean.Meta.Grind.Arith.Linear.getLeFn {m : Type → Type} [Monad m] [MonadError m] [MonadGetStruct m] : m Expr

def Lean.Meta.Grind.Arith.Linear.getLinearOrderInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getRingInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getCommRingInst : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.getOrderedRingInst : LinearM Expr

def Lean.Grind.Linarith.Poly.eval? (p : Poly) : Meta.Grind.Arith.Linear.LinearM (Option Std.Internal.Rat)

Tries to evaluate the polynomial p using the partial model/assignment built so far. The result is none if the polynomial contains variables that have not been assigned.

def Lean.Grind.Linarith.Poly.eval?.go (a : PArray Std.Internal.Rat) (v : Std.Internal.Rat) : Poly → Option Std.Internal.Rat

def Lean.Meta.Grind.Arith.Linear.IneqCnstr.satisfied (c : IneqCnstr) : LinearM LBool

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.satisfied (c : DiseqCnstr) : LinearM LBool

def Lean.Meta.Grind.Arith.Linear.resetAssignmentFrom (x : Var) : LinearM Unit

Resets the assignment of any variable bigger or equal to x.

def Lean.Meta.Grind.Arith.Linear.getVar (x : Var) : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.inconsistent : LinearM Bool

Returns true if the linarith state is inconsistent.

def Lean.Meta.Grind.Arith.Linear.eliminated (x : Var) : LinearM Bool

Returns true if x has been eliminated using an equality constraint.

def Lean.Meta.Grind.Arith.Linear.getOccursOf (x : Var) : LinearM VarSet

Returns occurrences of x.

def Lean.Meta.Grind.Arith.Linear.addOcc (x y : Var) : LinearM Unit

Adds y as an occurrence of x. That is, x occurs in lowers[y], uppers[y], or diseqs[y].

def Lean.Grind.Linarith.Poly.updateOccs (p : Poly) : Meta.Grind.Arith.Linear.LinearM Unit

Given p a polynomial being inserted into lowers, uppers, or diseqs, get its leading variable y, and adds y as an occurrence for the remaining variables in p.

partial def Lean.Grind.Linarith.Poly.updateOccs.go (y : Var) (p : Poly) : Meta.Grind.Arith.Linear.LinearM Unit

def Lean.Grind.Linarith.Poly.findVarToSubst (p : Poly) : Meta.Grind.Arith.Linear.LinearM (Option (Int × Var × Meta.Grind.Arith.Linear.EqCnstr))

Given a polynomial p, returns some (x, k, c) if p contains the monomial k*x, and x has been eliminated using the equality c.

def Lean.Grind.Linarith.Poly.gcdCoeffsAux : Poly → Nat → Nat

def Lean.Grind.Linarith.Poly.gcdCoeffs (p : Poly) : Nat

def Lean.Grind.Linarith.Poly.div (p : Poly) (k : Int) : Poly

def Lean.Grind.Linarith.Poly.pickVarToElim? (p : Poly) : Option (Int × Var)

Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.

def Lean.Grind.Linarith.Poly.pickVarToElim?.go (k : Int) (x : Var) (p : Poly) : Int × Var