Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Fty-extensions
Isar
Kestrel-utilities
Set
C
Syntax-for-tools
Formalized-subset
Mapping-to-language-definition
Input-files
Compilation-database
Printer
Output-files
Abstract-syntax-operations
Implementation-environments
Abstract-syntax
Abstract-syntax-trees
Expr
Exprp
Expr-case
Expr-binary
Expr-kind
Expr-unary
Expr-funcall
Expr-equiv
Expr-cond
Expr-complit
Expr-cast/sub-ambig
Expr-cast/mul-ambig
Expr-cast/logand-ambig
Expr-cast/call-ambig
Make-expr-cast/call-ambig
Expr-cast/call-ambig->type/fun
Expr-cast/call-ambig->inc/dec
Expr-cast/call-ambig->arg/rest
Change-expr-cast/call-ambig
Expr-cast/and-ambig
Expr-cast/add-ambig
Expr-arrsub
Expr-ident
Expr-alignof-ambig
Expr-va-arg
Expr-tycompat
Expr-string
Expr-offsetof
Expr-memberp
Expr-member
Expr-gensel
Expr-const
Expr-comma
Expr-cast
Expr-alignof
Expr-stmt
Expr-sizeof-ambig
Expr-sizeof
Expr-paren
Expr-label-addr
Expr-extension
Expr-fix
Expr-count
Type-spec
Exprs/decls/stmts
Binop
Stmt
Unop
Amb-expr/tyname
Dirdeclor
Asm-stmt
Dec/oct/hex-const
Simple-escape
Fsuffix
Attrib
Ident
Amb-decl/stmt
Dirabsdeclor
Type-qual
Decl-spec
Fundef
Struct-declon
Asm-name-spec
Amb-declor/absdeclor
Struni-spec
Param-declor
Declor
Stor-spec
Transunit-ensemble
Initdeclor
Absdeclor
Tyname
Keyword-uscores
Label
Align-spec
Expr-option
Spec/qual
Lsuffix
Hex-frac-const
Desiniter
Param-declon
Iconst
Dirabsdeclor-option
Dec-frac-const
Dec-core-fconst
Comp-stmt
Extdecl
Const-expr-option
Amb?-declor/absdeclor
Isuffix
Hex-core-fconst
Attrib-spec
Struct-declor
Escape
Decl
Amb?-expr/tyname
Initer
Ident-option
Bin-expo
Absdeclor-option
Statassert
Member-designor
Initer-option
Enum-spec
Declor-option
Const
Block-item
Hex-quad
Eprefix
Const-expr
Oct-escape
Inc/dec-op
Fun-spec
Dec-expo
Cprefix-option
Asm-name-spec-option
Amb?-decl/stmt
S-char
Isuffix-option
Genassoc
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Type-spec-option
Sign-option
Sign
Q-char
Iconst-option
H-char
Fundef-option
Asm-output
Asm-input
Designor
Const-option
Usuffix
Univ-char-name
Hprefix
Enumer
Attrib-name
Transunit
Asm-qual
Typequal/attribspec
Stringlit
Dec-expo-prefix
Bin-expo-prefix
Header-name
Cconst
Expr/tyname
Decl/stmt
Declor/absdeclor
Asm-clobber
Typequal/attribspec-list
Decl-spec-list
Stringlit-list
Spec/qual-list
Inc/dec-op-list
Desiniter-list
Attrib-spec-list
S-char-list
Q-char-list
Param-declon-list
H-char-list
Decl-list
C-char-list
Typequal/attribspec-list-list
Struct-declor-list
Struct-declon-list
Initdeclor-list
Genassoc-list
Extdecl-list
Block-item-list
Enumer-list
Ident-list
Filepath-transunit-map
Expr-list
Asm-qual-list
Asm-output-list
Asm-input-list
Asm-clobber-list
Type-spec-list
Stor-spec-list
Ident-set
Ident-option-set
Ident-list-list
Eprefix-option-list
Designor-list
Attrib-list
Abstract-syntax-irrelevants
Type-specifier-lists
Ascii-identifiers
Abstraction-mapping
Standard
Storage-specifier-lists
Code-ensembles
Purity
Make-self-code-ensemble
Concrete-syntax
Disambiguation
Validation
Gcc-builtins
Preprocessing
Parsing
Atc
Transformation-tools
Language
Representation
Insertion-sort
Pack
Soft
Bv
Imp-language
Ethereum
Event-macros
Java
Riscv
Bitcoin
Zcash
Yul
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Axe
Lists-light
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Expr
Expr-cast/call-ambig
This is a product type, introduced by
fty::deftagsum
in support of
expr
.
Fields
type/fun —
amb-expr/tyname
inc/dec —
inc/dec-op-list
arg/rest —
expr
Subtopics
Make-expr-cast/call-ambig
Basic constructor macro for
expr-cast/call-ambig
structures.
Expr-cast/call-ambig->type/fun
Get the
type/fun
field from a
expr-cast/call-ambig
.
Expr-cast/call-ambig->inc/dec
Get the
inc/dec
field from a
expr-cast/call-ambig
.
Expr-cast/call-ambig->arg/rest
Get the
arg/rest
field from a
expr-cast/call-ambig
.
Change-expr-cast/call-ambig
Modifying constructor for
expr-cast/call-ambig
structures.