def Lean.Meta.Grind.Arith.Linear.isLeInst (struct : Struct) (inst : Expr) : Bool

Equations

• Lean.Meta.Grind.Arith.Linear.isLeInst struct inst = match struct.leFn? with | some leFn => Lean.Meta.Grind.isSameExpr leFn.appArg! inst | x => false

def Lean.Meta.Grind.Arith.Linear.isLtInst (struct : Struct) (inst : Expr) : Bool

Equations

• Lean.Meta.Grind.Arith.Linear.isLtInst struct inst = match struct.ltFn? with | some ltFn => Lean.Meta.Grind.isSameExpr ltFn.appArg! inst | x => false

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

Equations

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

def Lean.Meta.Grind.Arith.Linear.propagateCommRingIneq (e lhs rhs : Expr) (strict eqTrue : Bool) : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.propagateIntModuleIneq (e lhs rhs : Expr) (strict eqTrue : Bool) : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.propagateIneq (e : Expr) (eqTrue : Bool) : GoalM Unit

Equations

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