Lean4
/-- Given a type `ty` (the type of a hypothesis in the context or a provided expression),
attempt to parse it as an inequality, and return `(a, b, strict, positive)`, where
`positive` means it is a negated inequality and `strict` means it is a strict inequality
(`a < b` or `a ≱ b`). `a` is always the lesser argument and `b` the greater one.
-/
def parseBound (ty : Expr) : MetaM (Expr × Expr × Bool × Bool) := do
let ty ← whnfR ty
if ty.isAppOfArity ``Not 1 then
let ty ← whnfR ty.appArg!
if ty.isAppOfArity ``LT.lt 4 then
pure (ty.appArg!, ty.appFn!.appArg!, false, false)
else if ty.isAppOfArity ``LE.le 4 then
pure (ty.appArg!, ty.appFn!.appArg!, true, false)
else
failure
else if ty.isAppOfArity ``LT.lt 4 then
pure (ty.appFn!.appArg!, ty.appArg!, true, true)
else if ty.isAppOfArity ``LE.le 4 then
pure (ty.appFn!.appArg!, ty.appArg!, false, true)
else
failure
