Representation of a Boolean variable.
(varp x) → bool
A variable is now represented as just a natural number, and the abstract data type wrapper described below is no longer used (we found it too hard to reason about). We're preserving the documentation below for reference, but it's no longer true.
Think of a VARIABLE as an abstract data type that represents a Boolean variable. A variable has an index that can be used to distinguish it from other variables. The interface for working with variables is simply:
In the implementation, variables are nothing more than natural numbers.
That is, varp is just natp, while
Why, then, bother with a variable type at all? We use (for efficiency) integer encodings of related data types like variables and literals. Treating these as separate types helps us avoid confusing them for one another when we write programs.
A very nice presentation of this idea is found in Type Kata: Distinguishing different data with the same underlying representation, a blog post by Edward Z. Yang.
(defun varp (x) (declare (xargs :guard t)) (let ((__function__ 'varp)) (declare (ignorable __function__)) (natp x)))
(defthm booleanp-of-varp (b* ((bool (varp x))) (booleanp bool)) :rule-classes :tau-system)
(defthm varp-compound-recognizer (equal (varp x) (natp x)) :rule-classes :compound-recognizer)