### 1Definitions and Checks

syntax

 (definec fn-name (param ...) :out-type body-expr)

 param = param-name :in-type
Defines the function fn-name.

; sum-n : Nat -> Nat
; Given n, return 0 + 1 + 2 + ... + n
 > (definec sum-n (n :nat) :nat (cond ((equal n 0) 0) (t ; else (+ n (sum-n (- n 1))))))

syntax

 (defunc fn-name (param-name ...) :input-contract in-ctc-expr :output-contract out-ctc-expr body-expr)
Defines the function fn-name.

; sum-n : Nat -> Nat
; Given n, return 0 + 1 + 2 + ... + n
 > (defunc sum-n (n) :input-contract (natp n) :output-contract (natp (sum-n n)) (cond ((equal n 0) 0) (t ; else (+ n (sum-n (- n 1))))))

 syntax(check= actual-expr expected-expr)
Checks that actual-expr and expected-expr are equal.

> (check= (sum-n 5) (+ 1 2 3 4 5))
> (check= (sum-n 0) 0)
> (check= (sum-n 3) 6)
> (check= (sum-n 4) -32)
 -------------------- FAILURE name:       check= location:   eval:7:0 actual:     10 expected:   -32 --------------------
> (check= (sum-n 4) 10)
> (check= (sum-n 100) 5050)

 syntax(defconst *name* expr)
Defines *name* as a constant with the value of expr. The *name* must start and end with a * character.

 > (defconst *num-letters* 26) > *num-letters* 26

 syntax(test? expr-with-free-vars)
Tests whether the expr-with-free-vars is always true when a bunch of different values are filled in for the free variables.

The simplest test?s, without free variables, just check that the expression produces true:

> (test? t)
> (test? nil)
 -------------------- FAILURE name:       check-t location:   eval:13:0 params:     '(nil) --------------------
> (test? (equal (sum-n 5) 15))
> (test? (< (sum-n 10) 100))
> (test? (integerp 36))
> (test? (integerp "not an integer"))
 -------------------- FAILURE name:       check-t location:   eval:17:0 params:     '(nil) --------------------
> (test? (equal (rev (list 7 8 9)) (list 9 8 7)))

Other test?s might use free variables to test that it works the same way for any values.

 > (test? (equal (rev (list a b c)) (list c b a))) > (test? (equal (app (list a b) (list c d)) (list a b c d)))

To test functions that work on only a certain types of data, you can guard tests with an implies form. The sum-n function works on natural numbers, so you can wrap (implies (natp x) ....) around the test expression to test it with only natural numbers.

> (test? (implies (natp x) (> (sum-n x) x)))
> (test? (implies (natp y) (< (sum-n y) (* y y))))
 > (test? (implies (natp n) (equal (sum-n n) (/ (* n (+ n 1)) 2))))