		Search-engine friendly clone of the ACL2 documentation.

Rulesets

Table-based alternative to ACL2's named theories.

Rulesets are like theories, but can be extended with additional rules after first being defined. That is, you can build up a ruleset incrementally, across many books, instead of having to define it all at once and having it be forever fixed.

Basic usage of rulesets is just like theories. You can:

Introduce rulesets with def-ruleset
Extend existing rulesets with add-to-ruleset.
Enable/disable rulesets with enable*, disable*, and e/d*

When we define a new package FOO, we often set up FOO::enable as an alias for enable*, to make using rulesets more convenient.

Advanced users can do some nifty things with rulesets, e.g., you can have a superior ruleset that contains other rulesets, and it will grow as you add rules to the contained rulesets.

A ruleset is actually a list of so-called ruleset designators. All ruleset operators, such as e/d* and def-ruleset, take arguments that are rulesets. See expand-ruleset for a discussion of ruleset designators and the corresponding theories that they represent.

Subtopics

Expand-ruleset: Expand rulesets to theories.
E/d*: Ruleset-aware version of e/d.
Ruleset: The ruleset associated with a given name
Def-ruleset: (def-ruleset name form) creates a new ruleset.
Get-ruleset: The ruleset associated with a given name
Disable*: Ruleset-aware version of disable.
Def-ruleset!: Same as def-ruleset except that it does not complain if the ruleset already exists, instead acting like add-to-ruleset in that case.
Enable*: Ruleset-aware version of enable.
Add-to-ruleset: (add-to-ruleset name form) adds additional rules to an existing ruleset.