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
Taspi
Bitcoin
Riscv
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
Bigmems
Builtins
Execloader
Aleo
Aleobft
Aleobft-static
Aleobft-stake2
Aleobft-dynamic
Aleobft-stake
Aleobft-proposals
Correctness
Definition
Initialization
Transitions
Transitions-accept
Transitions-certify
Transitions-propose
Events-possiblep
Elections
Events-next
Event-possiblep
Event-next
Transitions-commit
Transitions-augment
Dags
Path-to-author+round
Cert-causal-history
Cert-set-causal-history
Cert-previous-in-dag-p
Dag-closedp
Transitions-endorse
Transitions-advance
Blockchains
Anchors
States
Events
Reachability
Library-extensions
Leo
Solidity
Paco
Concurrent-programs
Bls12-377-curves
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Cert-causal-history
Cert-set-causal-history
Signature
(cert-set-causal-history certs dag) → hist
Arguments
certs
—
Guard
(
certificate-setp
certs)
.
dag
—
Guard
(
certificate-setp
dag)
.
Returns
hist
—
Type
(
certificate-setp
hist)
.