Major Section: ACL2-BUILT-INS
String-append takes two arguments, which are both strings (if the
guard is to be met), and returns a string obtained by concatenating
together the characters in the first string followed by those in the
second. Also see concatenate, noting that the macro call
(concatenate 'string str1 str2).expands to the call
(string-append str1 str2).
To see the ACL2 definition of this function, see pf.
