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
Atc
Syntax-for-tools
Abstract-syntax
Parser
Printer
Mapping-to-language-definition
Ldm-tyspec-list
Ldm-stmts/blocks
Ldm-block-item-list
Ldm-block-item
Ldm-stmt
Ldm-absdeclor-obj
Ldm-exprs
Ldm-declor-obj
Ldm-declor-fun
Ldm-dirdeclor-obj
Ldm-dirdeclor-fun
Ldm-dirabsdeclor-obj
Ldm-decl-tag
Ldm-transunit-ensemble
Ldm-structdecl
Ldm-decl-obj
Ldm-decl-fun
Ldm-extdecl
Ldm-fundef
Ldm-paramdeclor
Ldm-paramdecl
Ldm-stoclaspec-list
Ldm-isuffix-option
Ldm-dec/oct/hex-const
Ldm-tyname
Ldm-transunit
Ldm-structdecl-list
Ldm-paramdecl-list
Ldm-isuffix
Ldm-desiniter
Ldm-desiniter-list
Ldm-binop
Ldm-ident
Ldm-extdecl-list
Ldm-enumer-list
Ldm-enumer
Ldm-initer
Ldm-expr-option
Ldm-const
Ldm-lsuffix
Ldm-label
Ldm-iconst
Ldm-expr-list
Ldm-block-item-list
Ldm-expr
Ldm-block-item
Ldm-stmt
Read-files
Read-and-parse-files
Print-files
Parse-files
Concrete-syntax
Write-files
Print-and-write-files
Preprocessing
Language
Representation
Transformation-tools
Pack
Java
Taspi
Bitcoin
Des
Ethereum
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
Mapping-to-language-definition
Ldm-stmts/blocks
Ldm-stmt
Map a statement to a statement in the language definition.
Signature
(ldm-stmt stmt) → (mv erp stmt1)
Arguments
stmt
—
Guard
(
stmtp
stmt)
.
Returns
stmt1
—
Type
(
c::stmtp
stmt1)
.