evalPowZeroNat — Mathlib

Lean4
/-- The `positivity` extension which identifies expressions of the form `a ^ (0 : ℕ)`.
This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/
@[positivity _ ^ (0 : ℕ)]
def evalPowZeroNat : PositivityExt where
  eval {u α} _zα _pα
    e := do
    let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) |
      throwError"not ^"
    let _a ← synthInstanceQ q(Semiring $α)
    let _a ← synthInstanceQ q(PartialOrder $α)
    let _a ← synthInstanceQ q(IsOrderedRing $α)
    _ ← synthInstanceQ q(Nontrivial $α)
    pure (.positive (q(pow_zero_pos $a) : Expr))
Похожие утверждения