Operator spacing and docstring clarity in the hashing modules - #26
Merged
Conversation
Exponentiation is tight (u^2, xdiv^3, 2^k), except when both operands are long and parenthesized, as in the Euler-criterion show lines. * and / are tight between short atomic operands, with uniform spacing along chains of the same operator (2*lam*hL, but 3 * A * x^2). + and - are tight only when adding or subtracting 1 from a short atom (ta+1). One application operand gained parentheses where a tight caret would have misread: (I.xnum x₁)^2. The modules added on the hashing branch had drifted into spacing every operator; comments and docstrings are included in the pass. The generated VeluCertificates.lean already follows the convention and is untouched. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Several docstrings had the form "conclusion: argument", leaving the relationship between the two implicit. Join them with "by", "because", or "so" as the relationship warrants. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Style and documentation cleanup of the modules added in #19, split out of the indifferentiability counting-interface branch (#25) so that PR's review is not dominated by formatting noise.
The style commit applies the binding-reflecting operator spacing convention across the hashing modules: exponentiation is tight (
u^2,xdiv^3,2^k) except when both operands are long and parenthesized, as in the Euler-criterionshowlines;*and/are tight between short atomic operands, with uniform spacing along chains of the same operator (2*lam*hL, but3 * A * x^2).+and-are tight only when adding or subtracting 1 from a short atom (ta+1,k-1). Chained exponentiation is parenthesized to reflect its right associativity (b2k^(2^j), notb2k^2^j), and one application operand gained parentheses where a tight caret would misread ((I.xnum x₁)^2). Comments and docstrings are included in the pass. The generatedVeluCertificates.leanalready follows the convention and is untouched.The docs commit rewords docstrings that had the form "conclusion: argument", leaving the relationship implicit; they now join the two with "by", "because", or "so" as the relationship warrants.
🤖 Claude Opus 4.8