mystrings.html

module String

  type string

  constant empty_string : string

  function concat string string : string

  axiom concat_assoc : forall s1 s2 s3.
    concat (concat s1 s2) s3 = concat s1 (concat s2 s3)

  axiom concat_empty_left :  forall s. concat empty_string s = s

  axiom concat_empty_right :  forall s. concat s empty_string = s

  use import list.List

  function split string : list string

split s splits string s at spaces, eg split " a b cd e" gives "a";"b";"cd";"e"

end