Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
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
Atc
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Printer
Print-exprs/decls
Print-stmts/blocks
Print-expr
Pristate
Print-type-qual-list-list
Print-fileset
Print-dec/oct/hex-const
Priopt
Print-s-char
Print-fundef
Print-c-char
Print-decl-inline
Print-ident
Print-ident-list
Print-hex-core-fconst
Print-dec-core-fconst
Print-oct-digit-achar
Print-hex-frac-const
Print-hex-digit-achar
Print-dec-frac-const
Print-dec-digit-achar
Print-strunispec
Print-initdeclor-list
Print-file
Print-astring
Print-type-qual-list
Print-stringlit-list
Print-inc/dec-op-list
Print-cprefix-option
Print-binop
Print-asm-name-spec
Print-univ-char-name
Print-transunit
Print-simple-escape
Print-s-char-list
Print-isuffix-option
Print-indent
Print-fsuffix-option
Print-extdecl-list
Print-eprefix-option
Print-decl-list
Print-dec-expo-option
Print-char
Print-c-char-list
Print-stor-spec
Print-oct-escape
Print-initdeclor
Print-escape
Print-dec-expo-prefix
Print-cconst
Print-bin-expo-prefix
Dec-pristate-indent
Print-type-qual
Print-stringlit
Print-sign-option
Print-isuffix
Print-fconst
Print-dec-expo
Print-block
Print-bin-expo
Print-new-line
Print-lsuffix
Print-inc/dec-op
Print-hex-quad
Print-fun-spec
Print-fsuffix
Print-extdecl
Print-eprefix
Print-cprefix
Print-usuffix
Print-unop
Print-label
Print-iconst
Print-hprefix
Print-decl
Print-const
Print-chars
Print-sign
Print-oct-digit-achars
Print-hex-digit-achars
Print-dec-digit-achars
Print-stmt
Print-expr-list
Init-pristate
Print-structdecl-list
Inc-pristate-indent
Print-paramdeclor
Print-dirdeclor
Default-priopt
Print-structdeclor
Print-initer
Print-structdecl
Print-genassoc-list
Print-enumspec
Print-absdeclor
Print-desiniter-list
Print-const-expr
Print-attrib
Print-tyname
Print-structdeclor-list
Print-spec/qual-list
Print-paramdecl-list
Print-paramdecl
Print-designor-list
Print-declspec-list
Print-attrib-spec-list
Print-statassert
Print-spec/qual
Print-enumer-list
Print-dirabsdeclor
Print-desiniter
Print-declspec
Print-block-item-list
Print-attrib-spec
Print-attrib-list
Print-align-spec
Print-type-spec
Print-genassoc
Print-enumer
Print-designor
Print-declor
Print-block-item
Formalized-subset
Mapping-to-language-definition
Output-files
Input-files
Validator
Concrete-syntax
Preprocessing
Implementation-environments
Language
Representation
Transformation-tools
Pack
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Printer
Print-exprs/decls
Print-genassoc
Print a generic association.
Signature
(print-genassoc genassoc pstate) → new-pstate
Arguments
genassoc
—
Guard
(
genassocp
genassoc)
.
pstate
—
Guard
(
pristatep
pstate)
.
Returns
new-pstate
—
Type
(
pristatep
new-pstate)
.