# Zulip Chat Archive

## Stream: general

### Topic: more protected definition

#### Kenny Lau (May 13 2020 at 20:52):

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 (May 13 2020 at 20:53):

What we should do is not have `nat.pow`

#### Yury G. Kudryashov (May 13 2020 at 20:54):

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 (May 13 2020 at 21:00):

Can we define `monoid.pow`

such that it's defeq to `nat.pow`

? So there isn't a diamond?

#### Chris Hughes (May 13 2020 at 21:01):

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 (May 13 2020 at 21:21):

Or we can define `has_pow`

based on `has_one`

and `has_mul`

.

#### Jalex Stark (May 13 2020 at 21:22):

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 (May 13 2020 at 21:42):

I meant `has_pow M nat`

#### Johan Commelin (May 14 2020 at 03:59):

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.

Last updated: May 14 2021 at 03:27 UTC