chore: Refactorings for elementary number theory #1048
Conversation
This reverts commit db81698.
fredrik-bakke
changed the title
|
I'll flag this as ready for review also. Since @malarbol is also refactoring elementary number theory stuff, the branches shouldn't sit for too long without being merged. This PR mainly swaps |
| @@ -46,100 +46,55 @@ bezouts-lemma-eqn-to-int : | |||
| ( abs-ℤ | |||
| ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H) *ℤ y)) | |||
| bezouts-lemma-eqn-to-int x y H = | |||
| equational-reasoning | |||
There was a problem hiding this comment.
One advantage of equational reasoning was that at least it showed the individual steps. Since you remove this information, could you write an informal proof that explains the steps?
There was a problem hiding this comment.
My comment applies to all of the removals of equational reasoning below. I think I don't want to loose the information of what each of the steps is, because eventually we will want to do a more serious refactoring (i.e., one that is not just cosmetic) where we actually find a better proof. Then it will be useful to have all the information handy.
There was a problem hiding this comment.
Perhaps I'm not completely sold on removing the equational reasoning proofs without actually finding better proofs for Bezout's lemma.
|
Did you mean to close this PR? @fredrik-bakke |
WIP #1043