On Fri, Jul 4, 2008 at 7:40 AM, Gabriel Dos Reis wrote: > ... > I would not like to add to the confusion, but when thinking of this > problem one should also keep an eye on the status of Mapping. > What is it? Is it a domain constructor or a category constructor? >
Mapping (e.g. A->B) is clearly a domain constructor since we can write: x:A->B := ... A->B is the type of x. But 'with x:A->B' is a category object so we should be able to say: x:Category := with x:A->B in this sense 'with' is a (special) category constructor - rather like Record is a special domain constructor. The thing that makes it special (and therefore necessarily built-in) is that the name 'x' is significant. It becomes part of the object. Aldor makes names like 'x' a object of type Enumeration but I think this is artificial. Regards, Bill Page. ------------------------------------------------------------------------- Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW! Studies have shown that voting for your favorite open source project, along with a healthy diet, reduces your potential for chronic lameness and boredom. Vote Now at http://www.sourceforge.net/community/cca08 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
