std4#314

Stream: PR reviews

[Yuyang Zhao]

I can't change the label of std4#314. Also there still seems to be no consensus on renaming docs#Nat.bit.

[Mario Carneiro]

comment awaiting-review on the PR to change the label

[Yuyang Zhao]

I made std4#314 a couple months ago. Now I have time to come back to my PR and then I found that the files I modified have been moved to core. What should I do now?

[Yuyang Zhao]

Sorry, I just realized I've created a conversation before.
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/std4.23314

[Kim Morrison]

Yes. Would it be possible to minimize the number of new definitions, though? Can you get whatever performance improvement is available here without having to introduce Nat.bit, etc? (i.e. just inline the changes?)

[Eric Wieser]

Nat.bit is part of the type of binaryRec, so I think it would be quite unpleasant to remove unless we do so in mathlib first

[Eric Wieser]

I think bodd and div2 have no such property; but again, it probably makes sense to start by eliminating them from mathlib first.

[Yuyang Zhao]

lean4#3756 is ready for review