# Litp

Representation of a literal (a Boolean variable or its negation).

- Signature
(litp x) → bool

- Returns
`bool` — Type (booleanp bool).

Think of a **LITERAL** as an abstract data type that can either
represent a Boolean variable or its negation. More concretely, you can think
of a literal as an structure with two fields:

- var, a variable, represented as a natural number, and
- neg, a bit that says whether the variable is negated or not,
represented as a bitp.

In the implementation, we use an efficient natural-number encoding rather
than some kind of cons structure: neg is the bottom bit of the literal,
and var is the remaining bits. (This trick exploits the representation of
identifiers as natural numbers.)

### Definitions and Theorems

**Function: **litp

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

**Theorem: **booleanp-of-litp

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

**Theorem: **litp-compound-recognizer

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

### Subtopics

- Lit-negate-cond
- Efficiently negate a literal.
- Lit-negate
- Efficiently negate a literal.
- Make-lit
- Construct a literal with the given var and neg.
- Lit-equiv
- Basic equivalence relation for literals.
- Lit->var
- Access the var component of a literal.
- Lit->neg
- Access the neg bit of a literal.
- Lit-list
- List of literals
- Maybe-litp
- Recognizer for lits and nil.
- Lit-fix
- Basic fixing function for literals.
- Lit-list-list
- List of lit-lists