evalIntLCM — Mathlib

Lean4
/-- Extension for `Int.lcm`. -/
@[positivity Int.lcm _ _]
def evalIntLCM : PositivityExt where
  eval {u α} _ _
    e := do
    match u, α, e with
    | 0, ~q(ℕ), ~q(Int.lcm $a $b) =>
      let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
      let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
      assertInstancesCommute
      match (← core z p a).toNonzero with
      | some na =>
        match (← core z p b).toNonzero with
        | some nb =>
          return .positive q(Int.lcm_pos $na $nb)
        | _ =>
          failure
      | _ =>
        failure
    | _, _, _ =>
      throwError"not Int.lcm"
Похожие утверждения