Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Defbytelist
Defbyte-standard-instances
Defbyte-ihs-theorems
Defbyte-implementation
Defbyte-fn
Defbyte-infop
Defbyte-info
Make-defbyte-info
Change-defbyte-info
Make-honsed-defbyte-info
Honsed-defbyte-info
Defbyte-info->size
Defbyte-info->signed
Defbyte-check-size
Defbyte-fix-support-lemma
Defbyte-table
Defbyte-macro-definition
*defbyte-table-name*
Deffixequiv
Defresult
Deffixtype
Fty-discipline
Defoption
Fty-extensions
Defsubtype
Specific-types
Deftypes
Defflatsum
Defset
Deflist-of-len
Defbytelist
Fty::basetypes
Defvisitors
Deffixtype-alias
Defomap
Deffixequiv-sk
Defunit
Deffixequiv-mutual
Fty::baselists
Defmap
Std/util
Apt
Defdata
Defrstobj
Seq
Match-tree
Defrstobj
With-supporters
Def-partial-measure
Template-subst
Soft
Defthm-domain
Event-macros
Def-universal-equiv
Def-saved-obligs
With-supporters-after
Definec
Sig
Outer-local
Data-structures
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Defbyte-infop
Defbyte-info->size
Access the
size
field of a
defbyte-infop
structure.