Search-engine friendly clone of the
ACL2 documentation
.
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-p-sign->sign
Pnumber-number-upcase-p-sign->number
Make-pnumber-number-upcase-p-sign
Change-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
Pnumber
Pnumber-number-upcase-p-sign
This is a product type, introduced by
fty::deftagsum
in support of
pnumber
.
Fields
number —
pnumber
sign —
sign
Subtopics
Pnumber-number-upcase-p-sign->sign
Get the
sign
field from a
pnumber-number-upcase-p-sign
.
Pnumber-number-upcase-p-sign->number
Get the
number
field from a
pnumber-number-upcase-p-sign
.
Make-pnumber-number-upcase-p-sign
Basic constructor macro for
pnumber-number-upcase-p-sign
structures.
Change-pnumber-number-upcase-p-sign
Modifying constructor for
pnumber-number-upcase-p-sign
structures.