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
Expr-grade-<=
Binop-expected-grades
Expr->grade
Pprint-char
Pprint-console
Pprint-var/const-sort
Pprint-indent
Pprint-constdecl
Pprint-vardecl
Pprint-statement
Pprint-statement-list
Pprint-branch-list
Pprint-branch
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-statement
Pprint-branch
Signature
(pprint-branch branch level) → lines
Arguments
branch
—
Guard
(
branchp
branch)
.
level
—
Guard
(
natp
level)
.
Returns
lines
—
Type
(
msg-listp
lines)
.