Std/alists/abstract
Abstract theories for alist predicates
This book works similarly to std/lists/abstract, defining a set of
theorems about a generic alist using functions:
- keytype-p
- valtype-p
- keyval-alist-p
See std/lists/abstract for documentation of the general idea.
List of requirement variables recognized by std::deflist
Note: All of these are symbols in the ACL2 package.
- keytype-p-of-nil, valtype-p-of-nil, respectively, are true if NIL
is known to be a key/value
- not-keytype-p-of-nil, not-valtype-p-of-nil are true if NIL is
known not to be a key/value. ***-of-nil and not-***-of-nil may not
both be true, but may both be false in cases where the status of NIL is unknown
or depends on extra input parameters.
- key-negatedp, val-negatedp are true if we are creating an alist
that recognizes elements defined by NOT of the predicate, which may affect
the correct formulation of rewrite rules
- true-listp is true if the alist recognizer is strict, i.e., implies true-listp
- single-var is true if the alist recognizer has no extra parameters
- cheap is true if the user gave an extra option requesting cheaper versions of some rules.
Subtopics
- Keyval-alist-p
- Generic typed list recognizer function.
- Valtype-p
- Generic typed list valtype recognizer.
- Keytype-p
- Generic typed list keytype recognizer.
- Def-alistp-rule
- Define a theorem and save it in a table, denoting that it is a rule
about keyval-alistp.
