feat: add little-endian numeral notation conversions for positive, N, Z#278
Draft
JasonGross wants to merge 1 commit into
Draft
feat: add little-endian numeral notation conversions for positive, N, Z#278JasonGross wants to merge 1 commit into
JasonGross wants to merge 1 commit into
Conversation
Add little-endian conversion functions using the new Decimal.luint/lint, Hexadecimal.luint/lint, and Number.luint/lint wrapper types from corelib. These functions reverse the digit list and delegate to the existing big-endian converters, keeping the implementation minimal. The existing big-endian Number Notations are unchanged; the LE conversion functions are provided for downstream use. Depends on: rocq-prover/rocq#22135 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
JasonGross
force-pushed
the
littleendian-numeral-notation
branch
from
3b2aeec to
6261f8a
Compare
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.
Summary
of_luint/to_luint,of_lint/to_lint, etc.) forpositive,N, andZNumber Notationdeclarations with(little endian)option for all numeric scopeslia(zify) fails to recognize largenatliterals rocq#22122: with little-endian digit lists,zifycan provide smooth support for large number literalsDetails
The little-endian conversions simply reverse digits then delegate to existing big-endian conversions (for parsing), or skip the final reversal (for printing). For example:
Pos.of_luint d := Pos.of_uint (Decimal.rev d)Pos.to_luint p := Pos.to_little_uint p(already exists, was only used internally)Files changed
theories/PArith/BinPosDef.v+BinPos.v— positive conversionstheories/NArith/BinNatDef.v+BinNat.v— N conversionstheories/ZArith/BinIntDef.v+BinInt.v— Z conversionsDependency
Requires rocq-prover/rocq#22135 for the
(little endian)grammar option.Test plan
BinPosDef.vo,BinNatDef.vo,BinIntDef.vocompileBinPos.vo,BinNat.vo,BinInt.vocompile🤖 Generated with Claude Code