English
Given an expression, determine whether it encodes equality, less-or-equal, or less-than, returning the relation together with the corresponding sides and the type.
Русский
Для данного выражения определить, задаёт ли оно равенство, ≤ или <, возвращая связь и соответствующие стороны.
LaTeX
$$$$ \\text{ineq?}(e) = (\\text{relation}, a, b, c) $$$$
Lean4
/-- 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 ineq? (e : Expr) : MetaM (Ineq × Expr × Expr × Expr) := do
let e ← whnfR (← instantiateMVars e)
match e.eq? with
| some p =>
return (Ineq.eq, p)
| none =>
match e.le? with
| some p =>
return (Ineq.le, p)
| none =>
match e.lt? with
| some p =>
return (Ineq.lt, p)
| none =>
throwError "Not a comparison: {e}"
