Parsing inequalities in expressions

This file provides expression recognizers returning the Mathlib.Ineq comparison type.

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 Mathlib.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.

Equations

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

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 Mathlib.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.

Equations

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