English
Given an expression e, attempt to classify it as an inequality; if that fails, examine its negation and classify accordingly.
Русский
Пытаемся классифицировать выражение e как неравенство; если не удаётся, рассматриваем его отрицание и классифицируем.
LaTeX
$$$$ \\text{ineqOrNotIneq?}(e) = (\\text{flag}, \\text{relation}, a, b, c) $$$$
Lean4
/-- 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.
-/
def ineqOrNotIneq? (e : Expr) : MetaM (Bool × Ineq × Expr × Expr × Expr) := do
try
return (true, ← e.ineq?)
catch _ =>
let some e' := e.not? |
throwError "Not a comparison: {e}"
return (false, ← e'.ineq?)
