# Primitives

Replacements for car, cdr, etc., that respect the
*non-set convention*.

Since the osets library uses ordered lists as the underlying
representation of sets, at some point we have to use **list
primitives** (car, cdr, endp, cons) to operate on sets. A problem with using
these functions directly is that they do not follow the non-set convention.

The **non-set convention** is: set operations should treat improper
sets (i.e., non-nil atoms and lists that have duplicated or mis-ordered
elements) as the empty set. We adopt this convention throughout the library.
It allows most of our rewrite rules to have no setp hypotheses.

The primitive list functions do follow the non-set convention. For
instance:

- (car '(1 1 1)) = 1, but (car nil) = nil
- (cdr '(1 1 1)) = (1 1), but (cdr nil) = nil
- (cons 1 '(1 1 1)) = (1 1 1 1), but (cons 1 nil) = (1)
- (endp '(1 1 1)) = nil, but (endp nil) = t

These behaviors make it harder to reason about set operations that are
written directly in terms of the list primitives. When we try to do so, we
usually have to do lots of work to consider all the cases about whether the
inputs are ordered, etc.

To solve lots of these problems, we introduce new **set primitives** that
are mostly like the list primitives, except that they follow the non-set
convention. These primitives are:

- (head X) - the first element of a set, nil for non/empty sets
- (tail X) - all rest of the set, nil for non/empty sets
- (insert a X) - ordered insert of a into X
- (empty X) - recognizer for non/empty sets.

The general idea is that set operations should be written in terms of these
set primitives instead of the list primitives, and the definitions of the set
primitives should be kept disabled to avoid having to reason about the low
level structure of sets.

### Subtopics

- Setp
`(setp x)` recognizes well-formed ordered sets.- Insert
`(insert a x)` adds the element a to the set X.- Head
`(head x)` returns the smallest element in a set.- Tail
`(tail x)` returns the remainder of a set after removing its head.- Sfix
`(sfix x)` is a fixing function for sets.- Empty
`(empty x)` recognizes empty sets.