# Definec

Function definitions with contracts extending defunc.

### Examples

(definec f (x :nat y :nat) :nat
(+ x y))
(definec len (a :all) :nat
(if (atom a)
0
(+ 1 (len (rest a)))))
(definec app (x :tl y :tl) :tl
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
(definec square-list (l nat-list) nat-list
(if (endp l)
nil
(app (list (* (car l) (car l)))
(square-list (cdr l))))
:verbose t
:skip-tests t)

### Purpose

The macro definec is an extension of defunc
that makes it more convient to specify simple contracts.
For example, the expansions of

(definec f (x :nat y :nat) :nat
(+ x y))

and

(definec f (x nat y nat) nat
(+ x y))

are equivalent and include the following events.

(defunc f (x y)
:input-contract (and (natp x) (natp y))
:output-contract (natp (f x y))
(+ x y))
(defthm f-definec-fc-rule
(implies (force (and (natp x) (natp y)))
(natp (f x y)))
:rule-classes ((:forward-chaining :trigger-terms ((f x y)))))

Notice that nat was turned into natp. We convert type names into
the corresponding predicates using defdata and we
support all (the type of the ACL2 universe), tl (the type of
true-lists), int (the type of integers), bool (the type of booleans)
and all other types defdata knows.

When specifying types one can use keywords or regular symbols,
as shown above. It is important to put a space between
the variable name and the type, e.g., x:nat will lead to errors.

As the examples above show, the paramater types and the return type
are used to generate defunc contracts and then the rest of
the arguments are passed to defunc, so you can use all the
bells and whistles of defunc.