The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Dear all,

 

By the way, what about also reforming the module String someday ? I tend
to think that having an Haskell-like vision where string = list ascii
would be nicer than the current specialized pseudo-list type. This way,
many functions could be shared between String and List. Of course,
remain to be check that we could keep the specific parsing/printing
of strings even when string = list ascii...

 If I may add my 5 cents: I used to work quite extensively with strings in Coq and indeed I found the specialized type for strings a nuisance, so the first thing I did was to re-define it as list of characters (for precisely the reason mentioned by Pierre: being able to use list functions for strings). So I give +1 to this idea :)

  Best,

  Adam

-- 
Adam Koprowski  [http://adam-koprowski.net]

R&D @ MLstate   [http://mlstate.com]