William Sit <[EMAIL PROTECTED]> writes: | Bill: | | Rather than reply to your ??? point by point, what I was trying to say is that | in a set X equipped with several (let's say three) operations each of which | (with appropriate "unit" element that I ignore for simplicity) makes the set | into a monoid, these three operations can be notated, say, *, +, o, and these | are programmed in the domain constructor X using three formulas (but without | looking at the code, you won't know which formulas are used or which matches | with a particular notation). Assume that these operators are not following any | particular convention (so if X is a set of real-valued functions on a finite | field, * could mean 'max', + could mean pointwise multiplication, and o could | mean pointwise addition).
Membership is by assertion, so I don't think your objection has with respect to Martin's idea has anyting fundamental -- the compiler is not guessing. -- Gaby _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
