has_nat_cast

Stream: general

[Violeta Hernández]

What's up with this new typeclass? What's the purpose?

[Violeta Hernández]

It doesn't seem to introduce notation, and I'm not sure what lemmas it could possibly introduce

[Violeta Hernández]

Was it not desirable to have nat.unary_castautomatically defined?

[Yaël Dillies]

It's to provide coe : ℕ → α. It was formerly deduced from [has_zero α] [has_one α] [has_add α]. Relevant PR is #12182.

[Yaël Dillies]

The problem is that we want coe : ℕ → ℕ to be defeq to id, coe : ℕ → ℤ to be defeq to docs#int.of_nat, coe : ℕ → with_bot ℕ to be defeq to the other coe : ℕ → with_bot ℕ (so defeq to some), etc...

[Violeta Hernández]

Oh, that makes sense.

[Violeta Hernández]

image.png Shouldn't this be has_nat_cast instead of has_coe?

[Violeta Hernández]

Or is the idea that you only use has_nat_cast for monoids or some other algebraic structure stronger than what pre-games are?

[Yaël Dillies]

Probably it should, yeah.

[Eric Wieser]

Is docs#add_monoid_with_one true for pgame?

[Kevin Buzzard]

I'm not even sure addition is associative on pgame, and really one could argue that there are many candidates for one. The idea is that game is a more sensible notion; pgame is some kind of auxiliary notion used in the construction of game.

[Gabriel Ebner]

Shouldn't this be has_nat_cast instead of has_coe?

It could be, but it doesn't buy you much. All the nat.cast lemmas require add_monoid_with_one, which pgame isn't.

[Violeta Hernández]

Addition isn't neither commutative nor associative on pgame!

[Violeta Hernández]

I do disagree with there being many candidates for 1, {{ | } | } with the obvious indexing types seems like the only reasonable choice

[Violeta Hernández]

But that's a whole other topic

[Eric Rodriguez]

is it worth making one of these for the redefinition of char_p? Or should I just inline it into char_p?

[Eric Wieser]

I think just inline it

[Eric Wieser]

Since it would be the only data field

[Eric Rodriguez]

I was also going to set defn control of smul, although I guess there's no real point as usually for charp the cast will just be x smul 1

[Eric Wieser]

The main reason for has_nat_cast (if my understanding is correct) is to make things like docs#function.injective.monoid easy to state