Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
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
Expr
Exprs/decls
Binop
Unambiguity
Stmt
Stmtp
Stmt-case
Stmt-for-expr
Stmt-for-decl
Stmt-for-ambig
Stmt-equiv
Stmt-ifelse
Stmt-while
Stmt-switch
Stmt-labeled
Stmt-if
Stmt-dowhile
Stmt-kind
Stmt-return
Stmt-expr
Stmt-expr->expr?
Make-stmt-expr
Change-stmt-expr
Stmt-compound
Stmt-goto
Stmt-continue
Stmt-break
Stmt-fix
Stmt-count
Abstract-syntax-operations
Type-spec
Amb-expr/tyname
Dirdeclor
Unop
Attrib
Dec/oct/hex-const
Simple-escape
Dirabsdeclor
Decl
Amb-decl/stmt
Ident
Amb-declor/absdeclor
Type-qual
Transunit-ensemble
Paramdeclor
Asm-name-spec
Structdecl
Declor
Absdeclor
Stor-spec
Fundef
Align-spec
Lsuffix
Declspec
Hex-frac-const
Fun-spec
Expr-option
Dec-frac-const
Dec-core-fconst
Strunispec
Dirabsdeclor-option
Desiniter
Amb?-declor/absdeclor
Isuffix
Hex-core-fconst
Escape
Amb?-expr/tyname
Structdeclor
Spec/qual
Label
Const-expr-option
Bin-expo
Tyname
Fsuffix
Enumspec
Absdeclor-option
Paramdecl
Initer-option
Initer
Declor-option
Const
Block-item
Oct-escape
Inc/dec-op
Iconst
Hex-quad
Eprefix
Dec-expo
Cprefix-option
Const-expr
Asm-name-spec-option
Amb?-decl/stmt
S-char
Isuffix-option
Ident-option
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Sign-option
Iconst-option
Genassoc
Fundef-option
Const-option
Usuffix
Univ-char-name
Statassert
Designor
Sign
Hprefix
Attrib-spec
Stringlit
Initdeclor
Enumer
Dec-expo-prefix
Bin-expo-prefix
Extdecl
Cconst
Transunit
Expr/tyname
Decl/stmt
Declor/absdeclor
Abstraction-mapping
Type-qual-list
Spec/qual-list
Inc/dec-op-list
Declspec-list
S-char-list
Decl-list
C-char-list
Structdeclor-list
Structdecl-list
Paramdecl-list
Initdeclor-list
Genassoc-list
Extdecl-list
Desiniter-list
Stmts/blocks
File-paths
Enumer-list
Block-item-list
Type-qual-list-list
Stringlit-list
Filepath-transunit-map
Expr-list
Attrib-spec-list
Type-spec-list
Stor-spec-list
Ident-set
Ident-option-set
Ident-list
Designor-list
Attrib-list
Parser
Printer
Formalized-subset
Mapping-to-language-definition
Output-files
Input-files
Validator
Concrete-syntax
Preprocessing
Implementation-environments
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
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Stmt
Stmt-expr
This is a product type, introduced by
fty::deftagsum
in support of
stmt
.
Fields
expr? —
expr-option
Subtopics
Stmt-expr->expr?
Get the
expr?
field from a
stmt-expr
.
Make-stmt-expr
Basic constructor macro for
stmt-expr
structures.
Change-stmt-expr
Modifying constructor for
stmt-expr
structures.