Lean4
/-- Converts a proof by `norm_num` that `e` is a numeral, into a normalization as a monomial:
* `e = 0` if `norm_num` returns `IsNat e 0`
* `e = Nat.rawCast n + 0` if `norm_num` returns `IsNat e n`
* `e = Int.rawCast n + 0` if `norm_num` returns `IsInt e n`
* `e = NNRat.rawCast n d + 0` if `norm_num` returns `IsNNRat e n d`
* `e = Rat.rawCast n d + 0` if `norm_num` returns `IsRat e n d`
-/
def evalCast {α : Q(Type u)} (sα : Q(CommSemiring $α)) {e : Q($α)} : NormNum.Result e → Option (Result (ExSum sα) e)
| .isNat _ (.lit (.natVal 0)) p => do
assumeInstancesCommute
pure ⟨_, .zero, q(cast_zero $p)⟩
| .isNat _ lit p => do
assumeInstancesCommute
pure ⟨_, (ExProd.mkNat sα lit.natLit!).2.toSum, (q(cast_pos $p) :)⟩
| .isNegNat rα lit p => pure ⟨_, (ExProd.mkNegNat _ rα lit.natLit!).2.toSum, (q(cast_neg $p) : Expr)⟩
| .isNNRat dsα q n d p =>
pure ⟨_, (ExProd.mkNNRat sα dsα q n d q(IsNNRat.den_nz $p)).2.toSum, (q(cast_nnrat $p) : Expr)⟩
| .isNegNNRat dα q n d p =>
pure ⟨_, (ExProd.mkNegNNRat sα dα q n d q(IsRat.den_nz $p)).2.toSum, (q(cast_rat $p) : Expr)⟩
| _ => none
