• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
          • Omaps
          • Directed-untranslate
          • Include-book-paths
          • Ubi
          • Numbered-names
          • Digits-any-base
            • Defdigits
            • Nat=>lendian*
            • Group-lendian
            • Defdigit-grouping
              • Defdigit-grouping-implementation
            • Ungroup-lendian
            • Lendian=>nat
            • Defthm-dab-return-types
            • Bendian=>nat
            • Nat=>bendian*
            • Trim-bendian*
            • Trim-lendian*
            • Nat=>lendian
            • Dab-digit-list-fix
            • Nat=>bendian
            • Ungroup-bendian
            • Group-bendian
            • Digits=>nat-injectivity-theorems
            • Dab-digit-listp
            • Nat=>lendian+
            • Dab-basep
            • Nat=>bendian+
            • Digits=>nat=>digits-inverses-theorems
            • Trim-lendian+
            • Trim-bendian+
            • Nat=>digits=>nat-inverses-theorems
            • Dab-digitp
            • Group/ungroup-inverses-theorems
            • Dab-digit-fix
            • Nat=>digits-injectivity-theorems
            • Dab-base
            • Digits-any-base-pow2
            • Dab-base-fix
          • Context-message-pair
          • With-auto-termination
          • Make-termination-theorem
          • Theorems-about-true-list-lists
          • Checkpoint-list
          • Sublis-expr+
          • Integers-from-to
          • Prove$
          • Defthm<w
          • System-utilities-non-built-in
          • Integer-range-fix
          • Minimize-ruler-extenders
          • Add-const-to-untranslate-preprocess
          • Unsigned-byte-fix
          • Signed-byte-fix
          • Defthmr
          • Paired-names
          • Unsigned-byte-list-fix
          • Signed-byte-list-fix
          • Show-books
          • Skip-in-book
          • Typed-tuplep
          • List-utilities
          • Checkpoint-list-pretty
          • Defunt
          • Keyword-value-list-to-alist
          • Magic-macroexpand
          • Top-command-number-fn
          • Bits-as-digits-in-base-2
          • Show-checkpoint-list
          • Ubyte11s-as-digits-in-base-2048
          • Named-formulas
          • Bytes-as-digits-in-base-256
          • String-utilities
          • Make-keyword-value-list-from-keys-and-value
          • Defmacroq
          • Integer-range-listp
          • Apply-fn-if-known
          • Trans-eval-error-triple
          • Checkpoint-info-list
          • Previous-subsumer-hints
          • Fms!-lst
          • Zp-listp
          • Trans-eval-state
          • Injections
          • Doublets-to-alist
          • Theorems-about-osets
          • Typed-list-utilities
          • Book-runes-alist
          • User-interface
          • Bits/ubyte11s-digit-grouping
          • Bits/bytes-digit-grouping
          • Message-utilities
          • Subsetp-eq-linear
          • Oset-utilities
          • Strict-merge-sort-<
          • Miscellaneous-enumerations
          • Maybe-unquote
          • Thm<w
          • Defthmd<w
          • Io-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Digits-any-base

Defdigit-grouping

Generate specialized versions of the operations to group and ungroup digits in arbitrary bases, based on existing instances of defdigits.

Introduction

The defdigits macro generates specialized versions of the operations to convert between natural numbers and digits. This macro, defdigit-grouping, generates specialized versions of the operations to convert between digits in smaller bases and digits in larger bases.

The defdigit-grouping macro references the names of two existing calls of defdigits, which determine the smaller and larger bases, as well as the specialized conversions to use to define the grouping and ungrouping functions generated by defdigit-grouping.

General Form

(defdigit-grouping name
                   :smaller ...
                   :larger ...
                   :group-bendian ...
                   :group-lendian ...
                   :ungroup-bendian ...
                   :ungroup-lendian ...
                   :parents ...
                   :short ...
                   :long ...
  )

Inputs

name

A symbol that names the ensemble of the generated specialized grouping and ungrouping functions. This is used as the XDOC topic under which the XDOC topics for the generated events are put.

:smaller

The name of a previous successful call of defdigits. This determines the smaller base for grouping and ungrouping. Let base be the smaller base.

:larger

The name of a previous successful call of defdigits. This determines the larger base for grouping and ungrouping, which must be a positive power of base that is at least 2. Let exp be that positive power, so that the larger base is base^exp.

:group-bendian
:group-lendian
:ungroup-bendian
:ungroup-lendian

Symbols that specify the names to use for the generated functions (see details below).

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the ensemble of the generated specialized grouping and ungrouping functions.

Generated Events

group-bendian
group-lendian
ungroup-bendian
ungroup-lendian

Specialized versions of group-bendian, group-lendian, ungroup-bendian, and ungroup-lendian. These new functions are accompanied by theorems corresponding to the ones that accompany the original functions.

The generated events include XDOC documentation. They are all under an XDOC for the ensemble, whose name is specified in the name input.

Subtopics

Defdigit-grouping-implementation
Implementation of defdigit-grouping.