# Varp

Representation of a Boolean variable.

- Signature
(varp x) → bool

- Returns
`bool` — Type (booleanp 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:

`(varp x)` → bool
- Recognize valid identifiers.
- (make-var index) → id
- Construct an identifier with the given given a natural number index.
- (var->index id) → index
- Get the index from an identifier.

In the implementation, variables are nothing more than natural numbers.
That is, varp is just natp, while make-var and
var->index are logically just nfix and in the execution are the
identity.

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.

### Definitions and Theorems

**Function: **varp

(defun varp (x)
(declare (xargs :guard t))
(let ((__function__ 'varp))
(declare (ignorable __function__))
(natp x)))

**Theorem: **booleanp-of-varp

(defthm booleanp-of-varp
(b* ((bool (varp x))) (booleanp bool))
:rule-classes :tau-system)

**Theorem: **varp-compound-recognizer

(defthm varp-compound-recognizer
(equal (varp x) (natp x))
:rule-classes :compound-recognizer)

### Subtopics

- Varp-reasoning
- Basic rules for reasoning about identifiers.