namespace core.list

# Lists and their opperations
#
#
list   { a list of items - syntactic sugar [a, b, c, ...] produces a list a with
         head a and tail [b, c, ...]. The end of the list has no tail }
head   { the head of the list as in head(_h, _l) }
tail   { the tail of the list - either a list or none, as in tail(_h, _l) }
length { the length of the list - 1 if tail == none, length(tail)+1 otherwise }

co_domain(list, head)
co_domain(list, tail)

domain(integer, length)
co_domain(list, length)

and { tail can be nothing i.e. the end of the list or can be a list }
   (and(instance_of(_l, list), or(instance_of(_t, list), instance_of(_t, none))),
    tail(_t, _l))

and { length of none is 0 }
   (equal(_l, none),
    length(0, _l))
and { length of a list is one more than the length of its tail }
   (and(instance_of(_list, list), tail(_tail, _list)),
    and(and(length(_length, _list), length(_tail_length, _tail)),
        add_one(_length, _tail_length)))