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
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
C
Syntax-for-tools
Atc
Atc-implementation
Atc-abstract-syntax
Atc-pretty-printer
Pprint-expressions
Pprint-expr
Expr-grade
Pprint-obj-declor
Expr-grade-<=
Binop-expected-grades
Pprint-obj-declon
Expr->grade
Pprint-tyspecseq
Pprint-tag-declon
Pprint-struct-declon-list
Pprint-fun-declor
Pprint-file
Pprint-stmt
Pprint-block-item-list
Pprint-block-item
Pprint-struct-declon
Pprint-obj-adeclor
Pprint-initer
Pprint-fun-declon
Pprint-indent
Pprint-hex-const
Pprint-fileset
Pprint-dec-const
Pprinted-lines-to-file
Pprint-tyname
Pprint-param-declon-list
Pprint-oct-const
Pprint-iconst-length
Pprint-iconst
Pprint-const
Expr-grade-index
Pprint-param-declon
Pprint-label
Pprint-ident-list
Pprint-binop
Pprint-fundef
Pprint-file-to-filesystem
Pprint-ext-declon-list
Pprint-unop
Pprint-line
Pprint-ident
Pprint-ext-declon
Pprint-comma-sep
Pprint-transunit
Pprint-one-line
Pprinted-lines-to-channel
Pprint-one-line-blank
Pprint-line-blank
Atc-event-and-code-generation
Fty-pseudo-term-utilities
Atc-term-recognizers
Atc-input-processing
Atc-shallow-embedding
Atc-process-inputs-and-gen-everything
Atc-table
Atc-fn
Atc-pretty-printing-options
Atc-types
Atc-macro-definition
Atc-tutorial
Language
Representation
Transformation-tools
Pack
Event-macros
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Pprint-stmt
Pprint-block-item
Signature
(pprint-block-item item level options) → lines
Arguments
item
—
Guard
(
block-itemp
item)
.
level
—
Guard
(
natp
level)
.
options
—
Guard
(
pprint-options-p
options)
.
Returns
lines
—
Type
(
msg-listp
lines)
.