Search-engine friendly clone of the
ACL2 documentation
.
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
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
Process-syntheto-toplevel-fn
Translation
Language
Static-semantics
Abstract-syntax
Expression
Expression-sum-field-list
Type
Binary-op
Expression-product-field-list
Abstract-syntax-operations
Function-definition-list->header-list
Type-definition-list->name-list
Initializer-list->value-list
Function-header-list->name-list
Typed-variable-list->type-list
Typed-variable-list->name-list
Branch-list->condition-list
Alternative-list->name-list
Function-specifier
Expression-variable-list
Type-subset
Field-list->type-list
Field-list->name-list
Function-specification
Identifier
Toplevel
Function-definer
Function-header
Type-definer
Literal
Literal-case
Literal-fix
Literal-equiv
Literalp
Literal-string
Literal-integer
Make-literal-integer
Literal-integer->value
Change-literal-integer
Literal-character
Literal-boolean
Literal-kind
Type-product
Function-definition
Type-sum
Maybe-expression
Transform-argument-value
Transform
Theorem
Quantifier
Maybe-function-specification
Maybe-typed-variable
Maybe-type-definition
Maybe-function-header
Maybe-function-definition
Maybe-type-sum
Maybe-type-subset
Maybe-type-product
Maybe-type-definer
Maybe-theorem
Maybe-type
Initializer
Type-definition
Alternative
Unary-op
Typed-variable
Branch
Field
Transform-argument
Type-recursion
Program
Function-recursion
Typed-variable-list
Toplevel-name
Toplevel-list
Initializer-list
Expression-fixtypes
Toplevel-fn-names
Lookup-transform-argument
Function-definition-names
Type-definition-list
Transform-argument-list
Function-header-list
Function-definition-list
Alternative-list
Type-list
Identifier-set
Identifier-list
Field-list
Expression-list
Branch-list
Extract-default-param-alist
Create-arg-defaults-table
Outcome
Abstract-syntax-operations
Outcome-list
Outcomes
Process-syntheto-toplevel
Shallow-embedding
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Literal
Literal-integer
This is a product type, introduced by
fty::deftagsum
in support of
literal
.
Fields
value —
natp
Subtopics
Make-literal-integer
Basic constructor macro for
literal-integer
structures.
Literal-integer->value
Get the
value
field from a
literal-integer
.
Change-literal-integer
Modifying constructor for
literal-integer
structures.