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
Soft
C
Syntax-for-tools
Atc
Language
Representation
Transformation-tools
Simpadd0
Splitgso
Constant-propagation
Split-fn
Specialize
Split-all-gso
Copy-fn
Abstract-syntax-funcall-fun-rename-fn
Abstract-syntax-rename-fn
Exprs/decls/stmts-rename-fn
Typequal/attribspec-list-list-rename-fn
Typequal/attribspec-list-rename-fn
Structdeclor-list-rename-fn
Param-declon-list-rename-fn
Attrib-spec-list-rename-fn
Structdecl-list-rename-fn
Initdeclor-list-rename-fn
Block-item-list-rename-fn
Asm-output-list-rename-fn
Asm-input-list-rename-fn
Spec/qual-list-rename-fn
Genassoc-list-rename-fn
Desiniter-list-rename-fn
Designor-list-rename-fn
Decl-spec-list-rename-fn
Enumer-list-rename-fn
Attrib-list-rename-fn
Expr-list-rename-fn
Decl-list-rename-fn
Dirabsdeclor-option-rename-fn
Const-expr-option-rename-fn
Absdeclor-option-rename-fn
Initer-option-rename-fn
Expr-option-rename-fn
Declor-option-rename-fn
Typequal/attribspec-rename-fn
Member-designor-rename-fn
Amb-expr/tyname-rename-fn
Amb-decl/stmt-rename-fn
Amb-declor/absdeclor-rename-fn
Type-spec-rename-fn
Struni-spec-rename-fn
Structdeclor-rename-fn
Structdecl-rename-fn
Statassert-rename-fn
Spec/qual-rename-fn
Param-declor-rename-fn
Param-declon-rename-fn
Initer-rename-fn
Initdeclor-rename-fn
Genassoc-rename-fn
Enumspec-rename-fn
Dirdeclor-rename-fn
Dirabsdeclor-rename-fn
Desiniter-rename-fn
Designor-rename-fn
Decl-spec-rename-fn
Const-expr-rename-fn
Block-item-rename-fn
Attrib-spec-rename-fn
Attrib-rename-fn
Asm-stmt-rename-fn
Asm-output-rename-fn
Asm-input-rename-fn
Align-spec-rename-fn
Absdeclor-rename-fn
Tyname-rename-fn
Stmt-rename-fn
Label-rename-fn
Expr-rename-fn
Enumer-rename-fn
Declor-rename-fn
Decl-rename-fn
Copy-fn-extdecl
Copy-fn-filepath-transunit-map
Copy-fn-fundef
Copy-fn-transunit-ensemble
Copy-fn-extdecl-list
Copy-fn-transunit
Rename
Utilities
Insertion-sort
Pack
Bv
Imp-language
Event-macros
Java
Riscv
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Lists-light
Axe
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Abstract-syntax-rename-fn
Stmt-rename-fn
Signature
(stmt-rename-fn c$::stmt old-fn new-fn) → fty::result
Arguments
c$::stmt
—
Guard
(
stmtp
c$::stmt)
.
old-fn
—
Guard
(
identp
old-fn)
.
new-fn
—
Guard
(
identp
new-fn)
.
Returns
fty::result
—
Type
(
stmtp
fty::result)
.