Ralf Hemmecke <[EMAIL PROTECTED]> writes: > I would very much like to be able to use any fancy character to denote the > multiplication of a monoid (not just ASCII).
I strongly disagree on this point. Any character OK, i.e., defining some operation to be infix or postfix, but please stay with ASCII. You know, not all keyboards provide all symbols, and it's a pain to look for a certain symbol when you're on a conference in Prag or China. And no, I don't want to remember character codes. And no, I don't want to have to use a GUI, since I often work through a modem. I agree with > That Monoid/AbeleanMonoid should be resolved. I want to be able to say that > the positive integers are a Monoid wrt. + and wrt *. and > Of course it should also mean to have a way to specify the behaviour of > algorithms in a formal way so that programs can be checked > automatically. Proof checkers should, of course, also be written in that > language. However, I'm afraid, I don't have 27 years left. And, top issue on my priority list are dependent types. As everybody knows meanwhile. I want to get rid of that stupid ANY workaround in the series domains. Martin _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
