some operators to work with stings not included in the the standard library, for example to transform a positive integer in a binary string, or to extract tokens from a string

  • Nat2string returns a binary representation of n, i.e. a string of binary digits
    Pre/Post conds (n::isnat) => (isstring)
    Example nat2string:19 == 10011

  • Stringtokens returns a sequence of tokens from the input string, given a set of separators
    Pre/Post conds (separators::isseqof:isstring)(input::isstring) => (isseqof:isstring)
    Example StringTokens:< , and , , >: 'Fred, Wilma, Barney and Lucy'
    == < 'Fred' , 'Wilma' , 'Barney' , 'Lucy' >

PLaSM is Free Software and may be distributed under GNU LGPL