lp15 at cam.ac.uk
Wed Jul 4 12:18:39 CEST 2018
Well, there’s this:
> String.translate (fn c => if Char.isSpace c then "" else str c) " y e s ";
val it = "yes": string
No idea what Isabelle/ML does to these primitives however.
> On 4 Jul 2018, at 11:11, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> I just copied old code I inherited from Sascha Böhm and his Vampire noncommercial. For sure there are endlessly many ways in which we could make Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a "stripWhiteSpace" function that would do the trick. But string manipulation in ML is like pulling teeth. If you happen to know which function I can call, I'll gladly change the code.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev