1.4.11 Trees
Determines if x is lexicographically less than y. Works on any atomic input.
Returns true if
x is not a
cons pair.
Tests two symbols for equality.
Examples: |
| > (eq 'yes 'yes) | 't | | > (eq 'yes 'no) | '() |
|
Tests equality of two numbers, symbols, or characters.
Examples: |
| > (eql 'yes 'yes) | 't | | > (eql 'yes 'no) | '() | | > (eql 5 5) | 't | | > (eql #\a #\b) | '() | | > (eql #\5 5) | '() |
|
Returns
t if and only if
x is either a number, a symbol, or a character.
Tests
x and
y for equality. Returns
t if and only if they are the same value.
The identity function. Returns its argument unchanged.
Determines if the two given items are in lexicographic order.
Shorthand macros for compositions of
car and
cdr. For
instance,
(caddr x) is equivalent to
(car (cdr (cdr x))).
Examples: |
| eval:541:0: defconst: defined outside of begin-below | at: here | in: (defconst *tree* (cons (cons (cons (cons 0 1) (cons 2 | 3)) (cons (cons 4 5) (cons 6 7))) (cons (cons (cons 8 9) | (cons 10 11)) (cons (cons 12 13) (cons 14 15))))) | | > (caar *tree*) | eval:542:0: application: bad syntax | in: (top/error . *tree*) | | > (cdar *tree*) | eval:543:0: application: bad syntax | in: (top/error . *tree*) | | > (cadr *tree*) | eval:544:0: application: bad syntax | in: (top/error . *tree*) | | > (cddr *tree*) | eval:545:0: application: bad syntax | in: (top/error . *tree*) | | > (caaar *tree*) | eval:546:0: application: bad syntax | in: (top/error . *tree*) | | > (cdaar *tree*) | eval:547:0: application: bad syntax | in: (top/error . *tree*) | | > (cadar *tree*) | eval:548:0: application: bad syntax | in: (top/error . *tree*) | | > (cddar *tree*) | eval:549:0: application: bad syntax | in: (top/error . *tree*) | | > (caadr *tree*) | eval:550:0: application: bad syntax | in: (top/error . *tree*) | | > (cdadr *tree*) | eval:551:0: application: bad syntax | in: (top/error . *tree*) | | > (caddr *tree*) | eval:552:0: application: bad syntax | in: (top/error . *tree*) | | > (cdddr *tree*) | eval:553:0: application: bad syntax | in: (top/error . *tree*) | | > (caaaar *tree*) | eval:554:0: application: bad syntax | in: (top/error . *tree*) | | > (cdaaar *tree*) | eval:555:0: application: bad syntax | in: (top/error . *tree*) | | > (cadaar *tree*) | eval:556:0: application: bad syntax | in: (top/error . *tree*) | | > (cddaar *tree*) | eval:557:0: application: bad syntax | in: (top/error . *tree*) | | > (caadar *tree*) | eval:558:0: application: bad syntax | in: (top/error . *tree*) | | > (cdadar *tree*) | eval:559:0: application: bad syntax | in: (top/error . *tree*) | | > (caddar *tree*) | eval:560:0: application: bad syntax | in: (top/error . *tree*) | | > (cdddar *tree*) | eval:561:0: application: bad syntax | in: (top/error . *tree*) | | > (caaadr *tree*) | eval:562:0: application: bad syntax | in: (top/error . *tree*) | | > (cdaadr *tree*) | eval:563:0: application: bad syntax | in: (top/error . *tree*) | | > (cadadr *tree*) | eval:564:0: application: bad syntax | in: (top/error . *tree*) | | > (cddadr *tree*) | eval:565:0: application: bad syntax | in: (top/error . *tree*) | | > (caaddr *tree*) | eval:566:0: application: bad syntax | in: (top/error . *tree*) | | > (cdaddr *tree*) | eval:567:0: application: bad syntax | in: (top/error . *tree*) | | > (cadddr *tree*) | eval:568:0: application: bad syntax | in: (top/error . *tree*) | | > (cddddr *tree*) | eval:569:0: application: bad syntax | in: (top/error . *tree*) |
|
Examples: |
| > 'a | 'a | | > '(1 2 3 4) | '(1 2 3 4) |
|
Examples: |
| > `a | 'a | | > `(1 2 3 4) | '(1 2 3 4) |
|
Example: |
| > '(list ,a b c d) | '(list ,'a b c d) |
|
Substitutes every occurrence of
old with
new in the given
tree. Uses
eql as the test.
Calculates the size of a value. This is the default recursion
metric used for ACL2 termination proofs.
The size of a cons-pair is one more than the sum of the sizes of its
car and cdr. The size of an integer is its absolute value,
the size of a rational number is the sum of the sizes of its numerator and
denominator, and the size of a complex number is one more than the sum of the
sizes of its real and imaginary parts. The size of a string is its length. The
size of all other values (characters and symbols) is 0.