Miscellaneous ACL2 Stuff
- Bibtex Entries for the ACL2 workshops
- Managing ACL2 Packages
- A brief guide to working with packages in ACL2, covering everything from how to create packages, choose your package's symbols, and work with books based on packages.
- Canonicalize eq/eql functions to equal forms
- Efficient, simple rewrite rules that canonicalize most of the -eq, -eql, and -equal functions to their -equal forms. For example, this normalizes all uses of member, member-eq, and member-equal, so that you can reason about them more easily.
- Generating provably unique symbols
- This comes in two files: interface and implementation. It allows you to create a list of n unique symbols, none of which is t or nil, and proves that the resulting list has no duplicates and so forth.
- Generating pseudorandom numbers in ACL2
- This might be useful for testing functions on random inputs. It is a really simple multiplicative pseudorandom number generator based on STOBJs.
- Logic-mode term order and properties
- This code is an alternate implementation of ACL2's fn-count-evg and term order stuff, which is admissible in logic mode and is shown to satisfy the properties of asymmetry, transitivity. We show that the weak term order is also reflexive, and that the strict term order is irreflexive and also a trichotomy over pseudo-terms. In other words, a total order of psuedo-termps.
- Turn off garbage collection messages in GCL
- I frequently forget how to do this, so I've left these instructions for myself.