Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Zfc
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
C
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
Java
Riscv
Taspi
Bitcoin
Des
Ethereum
X86isa
Sha-2
Yul
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Axe
Aleo
Aleobft
Aleovm
Leo
Grammar
Early-version
Json2ast
Testing
Definition
Flattening
Abstract-syntax
Dynamic-semantics
Compilation
Static-semantics
Concrete-syntax
Pretty-printer
Pprint-expression-algorithm
Expr-grade
Pprint-expression
Pprint-expression-list
Pprint-struct-init-list
Pprint-struct-init
Expr-grade-<=
Binop-expected-grades
Expr->grade
Pprint-char
Pprint-console
Pprint-var/const-sort
Pprint-indent
Pprint-constdecl
Pprint-vardecl
Pprint-statement
Pprint-type
*binops-opcall-print-names*
Pprint-programdecl
Pprint-line
Pprint-group-literal
Pprint-funparam-list
*unops-opcall-print-names*
Pprint-literal
Pprint-coordinate
Pprint-char-list
Pprint-bitsize-to-utype
Pprint-bitsize-to-itype
Expr-grade-index
Pprint-unop
Pprint-programid
Pprint-importdecl
Pprint-identifier
Pprint-funparam
Pprint-compdecl
Pprint-binop
Pprint-locator
Pprint-compdecl-list
Pprint-address
Pprint-structdecl
Pprint-natural
Pprint-mappingdecl
Pprint-integer
Pprint-fundecl
Pprint-comma-separated
Pprint-boolean
Pprint-annotation-list
Pprint-topdecl-list
Pprint-importdecl-list
Pprint-topdecl
Pprint-annotation
Pprint-file
Pprint-line-blank
Grammar
Lexing-and-parsing
Input-pretty-printer
Output-pretty-printer
Unicode-characters
Concrete-syntax-trees
Symbols
Keywords
Bigmems
Builtins
Execloader
Solidity
Paco
Concurrent-programs
Bls12-377-curves
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Pprint-expression
Pprint-struct-init
Signature
(pprint-struct-init cinit) → part
Arguments
cinit
—
Guard
(
struct-initp
cinit)
.
Returns
part
—
Type
(
msgp
part)
.