Ralf, I have updated my example of one way to write an inductive type (as per our recent discussion with Gaby) so that I hope the structure of the definition is more clear. See:
http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes In particular I found it convenient to first implement an extension of Aldor's Union type to make it more "categorical", i.e. as a true co-product in the sense of category theory. See http://wiki.axiom-developer.org/SandBoxLimitsAndColimits This exercise makes me think that there may be a potential for developing a new library in Aldor and domains in Spad that would provide these and similar categorical constructs. I would be most interested in your comments on this approach. Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
