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
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Atc
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Printer
Formalized-subset
Mapping-to-language-definition
Ldm-type-spec-list
Ldm-stmts/blocks
Ldm-absdeclor-obj
Ldm-exprs
Ldm-dirdeclor-obj
Ldm-declor-obj
Ldm-declor-fun
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-isuffix-option
Ldm-dec/oct/hex-const
Ldm-stor-spec-list
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
Ldm-expr-list
Ldm-block-item-list
Ldm-stmt
Ldm-block-item
Output-files
Input-files
Validator
Implementation-environments
Concrete-syntax
Preprocessing
Language
Representation
Transformation-tools
Pack
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
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)
.