## Lesson 1. Lisp

First of all, every operation in Lisp is a function. Even very basic mathematical operations, such as addition. Secondly, functions are called in a different way than they are in mathematics or in most other languages. While in most languages, you might write `f(x, y)`

, in Lisp, you write `(f x y)`

.

The addition function is called `+`

. Try adding two numbers now: `(+ 1 2)`

*Tip: You can click on any code you see in this tutorial to insert it at the prompt.*

`list`

. Try creating a list: `(list 8 6 7 5 3 0 9)`

`(list ...)`

, the single quote marker also "quotes" the items inside of it. While `(list 1 2 (+ 1 2))`

would be the same as `(list 1 2 3)`

, `'(1 2 (+ 1 2))`

is the same as `(list 1 2 (list '+ 1 2))`

.
The single quoted + sign, `'+`

is called a "symbol". You can use the single quote to create symbols out of sequences of characters, such as `'not-found`

, `'valid`

, or `'rule-33`

.

`append`

concatenates two (or more) lists together. Try: `(append '(1 2 3) '(4 5 6))`

`"like this"`

. The two boolean values are `t`

(for true) and `nil`

(for false). Actually, any value (except `nil`

) is considered to be true for boolean tests. Use `t`

if no other value makes more sense.
The primary use for boolean functions and values is to branch using the `(if ...)`

function.

Usage: `(if test if-true if-false)`

Try it now with one of the simple boolean values: `(if t "True" "False")`

`(if ...)`

doesn't do much good here; you already know that t is true. You'll almost always call (if ...) with a function call for the second parameter. Here are some functions that return boolean values:
```
(< a b) (> a b) (<= a b) (>= a b) (= a b) (/= a b)
```

These are the six equality and inequality tests. They should be familiar to you. The final one is 'not equal'; the slash is meant to signify the crossed out equal sign of mathematics.

```
(integerp x) (rationalp x) (acl2-numberp x) (complex-rationalp x) (natp x)
```

These functions 'recognize' some of the different types of numbers available in ACL2 (that is, they return `t`

when their argument is of the requested type; `(integerp x)`

returns `t`

if `x`

is an integer). The terminal '`p`

' is a common idiom from Lisp and means "predicate". You can imagine it as a sort of question mark; `(natp i)`

means "Is `i`

an natural number?".

Try this: `(if (= (+ 1 3) (+ 5 2 -3)) "Equal" "Not equal")`

```
(endp xs) (listp xs) (true-listp xs) (equal xs ys)
```

These functions relate to lists. `(endp xs)`

checks to see if `xs`

is an empty list (if we are "at the end" of the list, a phrasing that makes sense if you think about these functions as they are used recursively). `(listp xs)`

is a recognizer for lists. `(true-listp xs)`

is a stronger recognizer for lists that checks to see if the marker used for the empty list is `nil`

, as it is in the system-created lists. Most ACL2 functions are intended to work with "true" lists, like the ones you can construct with `(list ...)`

. `(equal ...)`

tests the equality of lists (or more simple elements). `(= ...)`

is intended for numbers.

As a side note, I often use `xs`

(or `ys`

, `zs`

, etc), pronounced like English plurals ("exes", "whys", "zees"), for lists and `x`

, `y`

, etc. for numbers or simple values. This is just a convention, not a part of Lisp.

This time, try: `(true-listp '(a b c))`

to verify what I asserted earlier.

Instead, to produce meaningful or complex programs, you'll need to modify and return variables by creating new ones. This may seem unusual and may take some time to get accustomed to if you've never used an applicative programming language, but once you get the hang of it, it's pretty easy.

Lets start with aliases. They are a good way to "save" the results of a complex computation and use it more than once, so you don't have to redo expensive operations. Aliasing is done with the `let`

function.

```
(let ((alias1 value1) (alias2 value2) ...) body)
```

where the aliases are symbols, just like before (but without the ') and the values are either literal values, or, more often, function calls.

Try this: `(let ((xs (append '(1 2 3) '(4 5 6)))) (and (listp xs) (true-listp xs)))`

`(and ...)`

. It does what you'd expect from boolean algebra, and you can also use `(or ...)`

, `(not ...)`

, `(implies p q)`

, etc.
There's one final important built-in function that I'd like to introduce. To compute the length of a list, use (len xs): `(len '(1 2 3 4))`

.