nat.cast for enat

Stream: general

[Yaël Dillies]

Why is the coercion ℕ → enat not nat.cast? I'm having a hard time carrying the casts around.

[Johan Commelin]

For efficiency reasons, in the case you want to compute with enat?

[Eric Wieser]

Presumably it's definitionally more useful?

[Yaël Dillies]

I feel like enat has been designed for computation and not for reasoning... First, it's based on part. Second, it has its own cast.

[Yaël Dillies]

I'm currently stuck on

import algebra.big_operators.basic
import data.nat.enat

open_locale big_operators nat
open finset multiplicity nat

example {ι : Type*} {f : ι → ℕ} {s : finset ι} :
  ((∑ i in s, f i : ℕ) : enat) = ∑ i in s, f i := sorry

[Yakov Pechersky]

Prove that the cast is add_monoid_hom and then use docs#add_monoid_hom.map_sum