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
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
C
Syntax-for-tools
Disambiguator
Abstract-syntax
Expr
Exprp
Expr-case
Expr-kind
Expr-binary
Expr-equiv
Expr-cond
Expr-complit
Expr-cast/sub-ambig
Expr-cast/mul-ambig
Expr-cast/call-ambig
Expr-cast/and-ambig
Expr-cast/add-ambig
Expr-va-arg
Expr-unary
Expr-tycompat
Expr-offsetof
Expr-memberp
Expr-member
Expr-ident
Expr-gensel
Expr-funcall
Expr-comma
Expr-cast
Expr-arrsub
Expr-alignof
Expr-string
Expr-stmt
Expr-sizeof-ambig
Expr-sizeof
Expr-paren
Make-expr-paren
Expr-paren->inner
Change-expr-paren
Expr-extension
Expr-const
Expr-fix
Expr-count
Exprs/decls/stmts
Type-spec
Binop
Stmt
Amb-expr/tyname
Dirdeclor
Unop
Asm-stmt
Dec/oct/hex-const
Simple-escape
Attrib
Amb-decl/stmt
Dirabsdeclor
Ident
Decl-spec
Structdecl
Fundef
Asm-name-spec
Amb-declor/absdeclor
Transunit-ensemble
Paramdeclor
Declor
Type-qual
Absdeclor
Stor-spec
Keyword-uscores
Strunispec
Align-spec
Lsuffix
Label
Expr-option
Spec/qual
Hex-frac-const
Dec-frac-const
Dec-core-fconst
Tyname
Dirabsdeclor-option
Desiniter
Extdecl
Amb?-declor/absdeclor
Isuffix
Attrib-spec
Initdeclor
Hex-core-fconst
Escape
Decl
Const-expr-option
Amb?-expr/tyname
Structdeclor
Bin-expo
Statassert
Ident-option
Fsuffix
Enumspec
Absdeclor-option
Paramdecl
Member-designor
Initer-option
Initer
Declor-option
Const
Block-item
Oct-escape
Inc/dec-op
Iconst
Hex-quad
Fun-spec
Eprefix
Dec-expo
Cprefix-option
Const-expr
Asm-name-spec-option
Amb?-decl/stmt
S-char
Isuffix-option
Fundef-option
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Sign-option
Iconst-option
Genassoc
Asm-output
Asm-input
Const-option
Usuffix
Univ-char-name
Designor
Attrib-name
Sign
Hprefix
Asm-qual
Typequal/attribspec
Enumer
Dec-expo-prefix
Bin-expo-prefix
Stringlit
Transunit
Cconst
Expr/tyname
Decl/stmt
Declor/absdeclor
Asm-clobber
Typequal/attribspec-list
Stringlit-list
Inc/dec-op-list
Decl-spec-list
Spec/qual-list
S-char-list
Decl-list
C-char-list
Typequal/attribspec-list-list
Structdeclor-list
Structdecl-list
Paramdecl-list
Initdeclor-list
Genassoc-list
Filepath-transunit-map
Extdecl-list
Desiniter-list
Enumer-list
Block-item-list
Attrib-spec-list
Type-spec-list
Ident-list
Expr-list
Asm-qual-list
Asm-output-list
Asm-input-list
Asm-clobber-list
Stor-spec-list
Ident-set
Ident-option-set
Eprefix-option-list
Designor-list
Attrib-list
Parser
Validator
Printer
Formalized-subset
Mapping-to-language-definition
Defpred
Output-files
Input-files
Abstract-syntax-operations
Implementation-environments
Concrete-syntax
Unambiguity
Preprocessing
Abstraction-mapping
Annotation
Atc
Language
Representation
Transformation-tools
Pack
Event-macros
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Expr
Expr-paren
This is a product type, introduced by
fty::deftagsum
in support of
expr
.
Fields
inner —
expr
Subtopics
Make-expr-paren
Basic constructor macro for
expr-paren
structures.
Expr-paren->inner
Get the
inner
field from a
expr-paren
.
Change-expr-paren
Modifying constructor for
expr-paren
structures.