A function definition consists of a sequence of rules of the form
where Head is an atom or simple compound term, Commit
is a conjunct of goals, and Expression is a term. The
part of the rule is optional.
The heads of each rule of a relation have the same
functor and arity.
When the function is called, the rules are tried and the first rule whose
Head unifies with the function call and where Commit is
true then the result returned is the evaluation of Expression. Note that rules without an explicit Commit have an implicit
commit and so no backtracking occurs.
As examples, the definitions of the functions
tree2list are given below (using the tree type given above).
factorial : nat->nat factorial(0)->1 factorial(N) :: N1 = N-1 & type(N1,nat) -> N*factorial(N1) tree2list : tree(T) -> [T] tree2list(empty()) ->  tree2list(tr(LT, V, RT)) -> tree2list(LT) <> [V] <> tree2list(RT)
type(N1,nat) is necessary above in order that the type checker can type check the recursive call on