Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Deffixequiv
Defresult
Deffixtype
Fty-discipline
Defoption
Fty-extensions
Defsubtype
Specific-types
Deftypes
Deftagsum
Defprod
Defflexsum
Deflist
Defalist
Defoption
Deftranssum
Defmap
Defset
Defflatsum
Deflist-of-len
Defbytelist
Fty::basetypes
Defvisitors
Deffixtype-alias
Defomap
Deffixequiv-sk
Defunit
Deffixequiv-mutual
Fty::baselists
Defmap
Apt
Std/util
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
Deftypes
Deftranssum
Introduce a transparent sum of products. (beta)
BOZO document me.