Zulip Chat Archive

Stream: general

Topic: more protected definition


view this post on Zulip 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

view this post on Zulip Chris Hughes (May 13 2020 at 20:53):

What we should do is not have nat.pow

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 13 2020 at 21:21):

Or we can define has_pow based on has_one and has_mul.

view this post on Zulip 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 ℂ)

view this post on Zulip Yury G. Kudryashov (May 13 2020 at 21:42):

I meant has_pow M nat

view this post on Zulip 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