Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Gabriel Dos Reis]

William Sit <address@hidden> 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