Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Mmp-trees
Mmp-encode-n/c
Mmp-encode-c
Mmp-encode-u
Mmp-encode-n
Mmp-encode-c-max
Mmp-encode
Mmp-write
Mmp-decode
Mmp-encode-u-map
Nibblelist-bytelist-map-sup-len-key
Mmp-encode-c-forall
Mmp-read
Mmp-encoding-p
Bytelist-to-nibblelist-keys
Mmp-encode-c-exists
Bytelist-bytelist-map
Nibblelist-bytelist-map
Semaphore
Database
Cryptography
Rlp
Transactions
Hex-prefix
Basics
Addresses
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Mmp-encode-n/c
Mmp-encode-c
Signature
(mmp-encode-c map i) → (mv error? root database)
Arguments
map
—
Guard
(
nibblelist-bytelist-mapp
map)
.
i
—
Guard
(
natp
i)
.
Returns
error?
—
Type
(
member-eq
error? '(nil :collision :rlp))
.
root
—
Type
(
byte-listp
root)
.
database
—
Type
(
databasep
database)
.