Zulip Chat Archive

Stream: general

Topic: nat.cast for enat

Yaël Dillies (Aug 19 2021 at 17:54):

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

Johan Commelin (Aug 19 2021 at 19:06):

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

Eric Wieser (Aug 19 2021 at 19:41):

Presumably it's definitionally more useful?

Yaël Dillies (Aug 19 2021 at 20:05):

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 (Aug 19 2021 at 20:05):

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 (Aug 19 2021 at 20:09):

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

Last updated: Aug 03 2023 at 10:10 UTC