Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Community
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
Rename
Abstract-syntax-rename
Exprs/decls/stmts-rename
Filepath-transunit-map-rename
Extdecl-list-rename
Ident-list-rename
Typequal/attribspec-list-list-rename
Typequal/attribspec-list-rename
Structdeclor-list-rename
Param-declon-list-rename
Transunit-ensemble-rename
Structdecl-list-rename
Initdeclor-list-rename
Block-item-list-rename
Attrib-spec-list-rename
Asm-output-list-rename
Spec/qual-list-rename
Iconst-option-rename
Genassoc-list-rename
Desiniter-list-rename
Designor-list-rename
Decl-spec-list-rename
Asm-input-list-rename
Ident-option-rename
Const-option-rename
Attrib-list-rename
Enumer-list-rename
Expr-list-rename
Decl-list-rename
Attrib-name-rename
Extdecl-rename
Transunit-rename
Fundef-rename
Const-rename
Iconst-rename
Ident-rename
Dirabsdeclor-option-rename
Const-expr-option-rename
Absdeclor-option-rename
Initer-option-rename
Expr-option-rename
Declor-option-rename
Amb-declor/absdeclor-rename
Typequal/attribspec-rename
Member-designor-rename
Amb-expr/tyname-rename
Amb-decl/stmt-rename
Type-spec-rename
Tyname-rename
Strunispec-rename
Structdeclor-rename
Structdecl-rename
Stmt-rename
Statassert-rename
Spec/qual-rename
Param-declor-rename
Param-declon-rename
Label-rename
Initer-rename
Initdeclor-rename
Genassoc-rename
Expr-rename
Enumspec-rename
Enumer-rename
Dirdeclor-rename
Dirabsdeclor-rename
Desiniter-rename
Designor-rename
Declor-rename
Decl-spec-rename
Const-expr-rename
Block-item-rename
Attrib-spec-rename
Attrib-rename
Asm-stmt-rename
Asm-output-rename
Asm-input-rename
Align-spec-rename
Absdeclor-rename
Decl-rename
Ident-ident-subst
Ident-ident-alist
Utilities
Insertion-sort
Pack
Bv
Imp-language
Event-macros
Java
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
Align-spec-rename
Signature
(align-spec-rename c$::align-spec subst) → fty::result
Arguments
c$::align-spec
—
Guard
(
align-specp
c$::align-spec)
.
subst
—
Guard
(
ident-ident-alistp
subst)
.
Returns
fty::result
—
Type
(
align-specp
fty::result)
.