Ineq datatype

This file contains an enum Ineq (whose constructors are eq, le, lt), and operations involving it. The type Ineq is one of the fundamental objects manipulated by the linarith and linear_combination tactics.

Inequalities

inductive Mathlib.Ineq : Type

The three-element type Ineq is used to represent the strength of a comparison between terms.

• eq : Ineq
• le : Ineq
• lt : Ineq

instance Mathlib.instDecidableEqIneq : DecidableEq Ineq

instance Mathlib.instInhabitedIneq : Inhabited Ineq

def Mathlib.instInhabitedIneq.default : Ineq

instance Mathlib.instReprIneq : Repr Ineq

def Mathlib.instReprIneq.repr : Ineq → ℕ → Std.Format

def Mathlib.Ineq.max : Ineq → Ineq → Ineq

max R1 R2 computes the strength of the sum of two inequalities. If t1 R1 0 and t2 R2 0, then t1 + t2 (max R1 R2) 0.

def Mathlib.Ineq.cmp : Ineq → Ineq → Ordering

Ineq is ordered eq < le < lt.

def Mathlib.Ineq.toString : Ineq → String

Prints an Ineq as the corresponding infix symbol.

instance Mathlib.Ineq.instToString : ToString Ineq

instance Mathlib.Ineq.instToFormat : Std.ToFormat Ineq

Parsing inequalities

def Lean.Expr.ineq? (e : Expr) : MetaM (Mathlib.Ineq × Expr × Expr × Expr)

Given an expression e, parse it as a =, ≤ or <, and return this relation (as a Linarith.Ineq) together with the type in which the (in)equality occurs and the two sides of the (in)equality.

This function is more naturally in the Option monad, but it is convenient to put in MetaM for compositionality.

def Lean.Expr.ineqOrNotIneq? (e : Expr) : MetaM (Bool × Mathlib.Ineq × Expr × Expr × Expr)

Given an expression e, parse it as a =, ≤ or <, or the negation of such, and return this relation (as a Linarith.Ineq) together with the type in which the (in)equality occurs, the two sides of the (in)equality, and a Boolean flag indicating the presence or absence of the ¬.

This function is more naturally in the Option monad, but it is convenient to put in MetaM for compositionality.