Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
Process-syntheto-toplevel-fn
Translation
Language
Static-semantics
Abstract-syntax
Expression
Expression-sum-field-list
Type
Binary-op
Expression-product-field-list
Abstract-syntax-operations
Function-definition-list->header-list
Type-definition-list->name-list
Initializer-list->value-list
Function-header-list->name-list
Typed-variable-list->type-list
Typed-variable-list->name-list
Branch-list->condition-list
Alternative-list->name-list
Function-specifier
Function-specifier-fix
Function-specifier-case
Function-specifier-equiv
Function-specifierp
Function-specifier-quantified
Function-specifier-regular
Function-specifier-input-output
Function-specifier-input-output->relation
Make-function-specifier-input-output
Change-function-specifier-input-output
Function-specifier-kind
Expression-variable-list
Type-subset
Field-list->type-list
Field-list->name-list
Function-specification
Identifier
Toplevel
Function-definer
Function-header
Type-definer
Literal
Type-product
Function-definition
Type-sum
Maybe-expression
Transform-argument-value
Transform
Theorem
Quantifier
Maybe-function-specification
Maybe-typed-variable
Maybe-type-definition
Maybe-function-header
Maybe-function-definition
Maybe-type-sum
Maybe-type-subset
Maybe-type-product
Maybe-type-definer
Maybe-theorem
Maybe-type
Initializer
Type-definition
Alternative
Unary-op
Typed-variable
Branch
Field
Transform-argument
Type-recursion
Program
Function-recursion
Typed-variable-list
Toplevel-name
Toplevel-list
Initializer-list
Expression-fixtypes
Toplevel-fn-names
Lookup-transform-argument
Function-definition-names
Type-definition-list
Transform-argument-list
Function-header-list
Function-definition-list
Alternative-list
Type-list
Identifier-set
Identifier-list
Field-list
Expression-list
Branch-list
Extract-default-param-alist
Create-arg-defaults-table
Outcome
Abstract-syntax-operations
Outcome-list
Outcomes
Process-syntheto-toplevel
Shallow-embedding
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Function-specifier
Function-specifier-input-output
This is a product type, introduced by
fty::deftagsum
in support of
function-specifier
.
Fields
relation —
expression
Subtopics
Function-specifier-input-output->relation
Get the
relation
field from a
function-specifier-input-output
.
Make-function-specifier-input-output
Basic constructor macro for
function-specifier-input-output
structures.
Change-function-specifier-input-output
Modifying constructor for
function-specifier-input-output
structures.