Generally useful macros for writing more concise code, and frameworks for quickly introducing concepts like typed structures, typed lists, defining functions with type signatures, and automating other common tasks.
Subtopics 
- Apt
- APT (Automated Program Transformations) is a library of tools to transform programs and program specifications with automated support.
- B*
- The b* macro is a replacement for let* that adds support for multiple return values, mixing control flow with binding, causing side effects, introducing type declarations, and doing other kinds of custom pattern matching.
- Data-structures
- The books/data-structures library
- Def-partial-measure
- Introduce measure and termination predicates for a partial function definition
- Def-saved-obligs
- Save the proof obligations for a given event as separate defthms.
- Def-universal-equiv
- A macro for defining universally quantified equivalence relations.
- Defdata
- A Data Definition Framework
- Definec
- Function definitions with contracts extending defunc.
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs with the reasoning efficiency of records. They are designed for modeling, e.g., the state of a processor or virtual machine.
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs with the reasoning efficiency of records. They are designed for modeling, e.g., the state of a processor or virtual machine.
- Defthm-domain
- Prove termination on a given domain
- Defunc
- Function definitions with contracts. See also definec and defun.
- Event-macros
- A library of concepts and utilities for event macros.
- Fty
- FTY is a macro library for introducing new data types and writing type-safe programs in ACL2. It automates a systematic discipline for working with types that allows for both efficient reasoning and execution.
- Match-tree
- Match an object against a flexible pattern and return the unifying substitution
- Outer-local
- Support for events that are local to the outer context.
- Seq
- Seq is a macro language for applying actions to a stream.
- Sig
- Specify type signatures for polymorphic functions
- Soft
- SOFT (Second-Order Functions and Theorems) is a tool to mimic second-order functions and theorems in the first-order logic of ACL2.
- Std/util
- A macro library that automates defining types, introducing typed functions, mapping over lists, and many other boilerplate tasks.
- Template-subst
- Template-subst is a function for manipulating templates that may be used to generate events.
- With-supporters
- Automatically include specified definitions from a specified book
- With-supporters-after
- Automatically define necessary redundant definitions from after a specified event
0 comments:
Post a Comment