def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.applyEq? (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DiseqCnstr) : LinearM (Option DiseqCnstr)

Given an equation c₁ containing the monomial a*x, and a disequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

def Lean.Meta.Grind.Arith.Linear.inSameStruct? (a b : Expr) : GoalM (Option Nat)

Returns some structId if a and b are elements of the same structure.

def Lean.Meta.Grind.Arith.Linear.EqCnstr.norm (c : EqCnstr) : LinearM (Nat × Var × EqCnstr)

partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.applySubsts (c : EqCnstr) : LinearM EqCnstr

def Lean.Meta.Grind.Arith.Linear.IneqCnstr.applyEq (a : Nat) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : IneqCnstr) : LinearM IneqCnstr

Given an equation c₁ containing the monomial a*x, and an inequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.ignore (c : DiseqCnstr) : LinearM Unit

partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.applySubsts? (c₂ : DiseqCnstr) : LinearM (Option DiseqCnstr)

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.assert (c : DiseqCnstr) : LinearM Unit

def Lean.Meta.Grind.Arith.Linear.EqCnstr.assert (c : EqCnstr) : LinearM Unit

@[export lean_process_linarith_eq]

def Lean.Meta.Grind.Arith.Linear.processNewEqImpl (a b : Expr) : GoalM Unit

@[export lean_process_linarith_diseq]

def Lean.Meta.Grind.Arith.Linear.processNewDiseqImpl (a b : Expr) : GoalM Unit