On Wed, 2004-06-23 at 21:25, Richard Jones wrote:
> I also wonder if String.replace wouldn't be simpler and faster if the
> f function was defined as:
> f : char -> string option
The replace function would be more complex obviously,
however the client conversion function would be simpler
and the total result faster I think, so I think I'd
tend to support Richard's suggestion here.
Interesting this wouldn't be so in Python, which has
a very efficient string representation (and needs it
since there is no concept of a char).
John Skaller, mailto:skaller@...
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net