evalRatNum — Mathlib

Lean4
/-- The `positivity` extension which identifies expressions of the form `Rat.num a`,
such that `positivity` successfully recognises `a`. -/
@[positivity Rat.num _]
def evalRatNum : PositivityExt where
  eval {u α} _ _
    e := do
    match u, α, e with
    | 0, ~q(ℤ), ~q(Rat.num $a) =>
      let zα : Q(Zero ℚ) := q(inferInstance)
      let pα : Q(PartialOrder ℚ) := q(inferInstance)
      assumeInstancesCommute
      match ← core zα pα a with
      | .positive pa =>
        pure <| .positive q(num_pos_of_pos $pa)
      | .nonnegative pa =>
        pure <| .nonnegative q(num_nonneg_of_nonneg $pa)
      | .nonzero pa =>
        pure <| .nonzero q(num_ne_zero_of_ne_zero $pa)
      | .none =>
        pure .none
    | _, _ =>
      throwError"not Rat.num"
Похожие утверждения