Expr-option-replace-field-access
- Signature
(expr-option-replace-field-access c$::expr-option original
linkage new1 new2 split-members)
→
fty::result- Arguments
- c$::expr-option — Guard (expr-optionp c$::expr-option).
- original — Guard (identp original).
- linkage — Guard (c$::linkagep linkage).
- new1 — Guard (identp new1).
- new2 — Guard (identp new2).
- split-members — Guard (ident-listp split-members).
- Returns
- fty::result — Type (expr-optionp fty::result).
Definitions and Theorems
Theorem: expr-option-replace-field-access-under-iff
(defthm expr-option-replace-field-access-under-iff
(iff
(expr-option-replace-field-access c$::expr-option original
linkage new1 new2 split-members)
c$::expr-option))
