more protected definition

Stream: general

[Kenny Lau]

should we make stuff like nat.pow_two protected so that it doesn't clash with pow_two? this seems to be the approach with core lean

[Chris Hughes]

What we should do is not have nat.pow

[Yury G. Kudryashov]

AFAIR, nat.pow has a native implementation, so the plan is to delete the has_pow instance, and add a simp lemma from nat.pow to has_pow.pow.

[Chris Hughes]

Can we define monoid.pow such that it's defeq to nat.pow? So there isn't a diamond?

[Chris Hughes]

I tried redefining monoid.pow so a ^ (n+1) = a ^ n * a, as opposed to a * a^n. Now nat.pow._main is defeq to monoid.pow._main, but nat.pow is not defeq to monoid.pow

[Yury G. Kudryashov]

Or we can define has_pow based on has_one and has_mul.

[Jalex Stark]

Yury G. Kudryashov said:

Or we can define has_pow based on has_one and has_mul.

? don't we have an instance has_pow ℂ ℂ? (the point being that that instance is not constructed from has_one ℂ and has_mul ℂ)

[Yury G. Kudryashov]

I meant has_pow M nat

[Johan Commelin]

Kenny Lau said:

should we make stuff like nat.pow_two protected so that it doesn't clash with pow_two? this seems to be the approach with core lean

I agree with the rest that was said. But I think we can still make nat.pow_two protected. It's easy to do, and relieves some of our pains.