		Search-engine friendly clone of the ACL2 documentation.

Amb-expr/tyname-replace-field-access

Signature
(amb-expr/tyname-replace-field-access c$::amb-expr/tyname original linkage new1 new2 split-members) → fty::result
Arguments: c$::amb-expr/tyname — Guard (c$::amb-expr/tyname-p c$::amb-expr/tyname).; 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 (c$::amb-expr/tyname-p fty::result).