• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
            • Gcc-builtins
            • Preprocessing
              • Preprocessor
                • Preprocessor-states
                  • Plexeme
                  • Ppstate
                  • Pnumber
                    • Pnumber-count
                    • Pnumber-fix
                    • Pnumberp
                    • Pnumber-case
                    • Pnumber-equiv
                    • Pnumber-number-nondigit
                    • Pnumber-number-digit
                    • Pnumber-number-upcase-p-sign
                    • Pnumber-number-upcase-e-sign
                    • Pnumber-number-locase-p-sign
                    • Pnumber-number-locase-e-sign
                    • Pnumber-dot-digit
                    • Pnumber-digit
                    • Pnumber-number-dot
                    • Pnumber-kind
                  • Macro-info
                  • Macro-add
                  • Init-ppstate
                  • Plexeme-token/newline-p
                  • Newline
                  • Plexeme-option
                  • Macro-info-option
                  • Macro-table
                  • Plexeme+span
                  • Update-ppstate->lexemes-unread
                  • Update-ppstate->lexemes-read
                  • Update-ppstate->lexemes-length
                  • Update-ppstate->chars-unread
                  • Update-ppstate->chars-read
                  • Update-ppstate->version
                  • Update-ppstate->position
                  • Update-ppstate->macros
                  • Update-ppstate->chars-length
                  • Macro-lookup
                  • Update-ppstate->bytes
                  • Update-ppstate->size
                  • Plexeme-token/space-p
                  • Plexeme-tokenp
                  • Ppstate->gcc
                  • Plexeme-list-token/space-p
                  • Ppstate->size
                  • Ppstate->lexemes-unread
                  • Ppstate->lexemes-read
                  • Ppstate->lexemes-length
                  • Ppstate->chars-unread
                  • Ppstate->bytes
                  • Plexeme-list-token/newline-p
                  • Plexeme-list-not-token/newline-p
                  • Ident-macroinfo-alist
                  • Update-ppstate->lexeme
                  • Update-ppstate->char
                  • Ppstate->version
                  • Ppstate->macros
                  • Ppstate->chars-read
                  • Ppstate->chars-length
                  • Plexeme-list-tokenp
                  • Plexeme-list-not-tokenp
                  • Macro-table-init
                  • Ppstate->lexeme
                  • Ppstate->char
                  • Ppstate-fix
                  • Plexeme+span-list
                  • Plexeme-list
                  • Irr-pnumber
                  • Irr-plexeme
                  • Irr-macro-table
                  • Ppstate->position
                • Preprocessor-printer
                • Pread-token/newline
                • Pread-token
                • Preprocessor-lexer
                • Pproc-files
                • Pproc-file
                • Filepath-plexeme-list-alist-to-filepath-filedata-map
                • Filepath-plexeme-list-alist
                • Preprocessor-reader
                • Preprocessor-messages
              • External-preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Preprocessor-states

Pnumber

Fixtype of preprocessing numbers [C17:6.4.8] [C17:A.1.9].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:digit → pnumber-digit
:dot-digit → pnumber-dot-digit
:number-digit → pnumber-number-digit
:number-nondigit → pnumber-number-nondigit
:number-locase-e-sign → pnumber-number-locase-e-sign
:number-upcase-e-sign → pnumber-number-upcase-e-sign
:number-locase-p-sign → pnumber-number-locase-p-sign
:number-upcase-p-sign → pnumber-number-upcase-p-sign
:number-dot → pnumber-number-dot

This is like an abstract syntax for preprocessing numbers, corresponding to the rule for pp-number in the ABNF grammar. We need to capture their structure, in order to do preprocessing.

Subtopics

Pnumber-count
Measure for recurring over pnumber structures.
Pnumber-fix
Fixing function for pnumber structures.
Pnumberp
Recognizer for pnumber structures.
Pnumber-case
Case macro for the different kinds of pnumber structures.
Pnumber-equiv
Basic equivalence relation for pnumber structures.
Pnumber-number-nondigit
Pnumber-number-digit
Pnumber-number-upcase-p-sign
Pnumber-number-upcase-e-sign
Pnumber-number-locase-p-sign
Pnumber-number-locase-e-sign
Pnumber-dot-digit
Pnumber-digit
Pnumber-number-dot
Pnumber-kind
Get the kind (tag) of a pnumber structure.