Lean4
/-- Extension for Rat.cast. -/
@[positivity Rat.cast _]
def evalRatCast : PositivityExt where
eval {u α} _zα _pα
e := do
let ~q(@Rat.cast _ (_) ($a : ℚ)) := e |
throwError"not Rat.cast"
match ← core q(inferInstance) q(inferInstance) a with
| .positive pa =>
let _oα ← synthInstanceQ q(Field $α)
let _oα ← synthInstanceQ q(LinearOrder $α)
let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
assumeInstancesCommute
return .positive q((Rat.cast_pos (K := $α)).mpr $pa)
| .nonnegative pa =>
let _oα ← synthInstanceQ q(Field $α)
let _oα ← synthInstanceQ q(LinearOrder $α)
let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
assumeInstancesCommute
return .nonnegative q((Rat.cast_nonneg (K := $α)).mpr $pa)
| .nonzero pa =>
let _oα ← synthInstanceQ q(DivisionRing $α)
let _cα ← synthInstanceQ q(CharZero $α)
assumeInstancesCommute
return .nonzero q((Rat.cast_ne_zero (α := $α)).mpr $pa)
| .none =>
pure .none
