evalNNRatNum — Mathlib

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