Ralf Hemmecke <[EMAIL PROTECTED]> writes:
[...]
| ++ A set over a domain D models the usual mathematical notion of a
| ++ finite set of elements from D.
|
| Although
|
| i: Integer
|
| and
|
| s: FinitePowerSet T
|
| would be in perfect analogy if one read ":" as "element of", then to
| go on "l: List T" would mean "List" is the container of all finite
| sequences (with some information about their representation (linked
| list)).
And that would match the usual definition of List as the least fixed
point of the functor
X |-> 1 + X
in CPO.
However, the existence of 1.. in Axiom would suggest that actually
some people think of List as the greatest fixed point.
-- Gaby
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
