evalNNRatCast — Mathlib

Lean4
/-- Extension for NNRat.cast. -/
@[positivity NNRat.cast _]
def evalNNRatCast : PositivityExt where
  eval {u α} _zα _pα
    e := do
    let ~q(@NNRat.cast _ (_) ($a : ℚ≥0)) := e |
      throwError"not NNRat.cast"
    match ← core q(inferInstance) q(inferInstance) a with
    | .positive pa =>
      let _oα ← synthInstanceQ q(Semifield $α)
      let _oα ← synthInstanceQ q(LinearOrder $α)
      let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
      assumeInstancesCommute
      return .positive q((NNRat.cast_pos (K := $α)).mpr $pa)
    | _ =>
      let _oα ← synthInstanceQ q(Semifield $α)
      let _oα ← synthInstanceQ q(LinearOrder $α)
      let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
      assumeInstancesCommute
      return .nonnegative q(NNRat.cast_nonneg _)
Похожие утверждения