evalPosPart — Mathlib

Lean4
/-- Extension for `posPart`. `a⁺` is always nonnegative, and positive if `a` is. -/
@[positivity _⁺]
def evalPosPart : PositivityExt where
  eval {u α} zα pα
    e := do
    match e with
    | ~q(@posPart _ $instαpospart $a) =>
      let _instαlat ← synthInstanceQ q(Lattice $α)
      let _instαgrp ← synthInstanceQ q(AddGroup $α)
      assertInstancesCommute
        -- FIXME: There seems to be a bug in `Positivity.core` that makes it fail (instead of returning
            -- `.none`) here sometimes. See e.g. the first test for `posPart`. This is why we need
            -- `catchNone`

      match ← catchNone (core zα pα a) with
      | .positive pf =>
        return .positive q(posPart_pos $pf)
      | _ =>
        return .nonnegative q(posPart_nonneg $a)
    | _ =>
      throwError"not `posPart`"
Похожие утверждения