String-append
concatenate two strings
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. For a related macro that can take an arbitrary number of string
arguments, see concatenate, noting that the macro call
(concatenate 'string str1 str2).
expands to the call
(string-append str1 str2).
Function: string-append
(defun string-append (str1 str2)
(declare (xargs :guard (and (stringp str1) (stringp str2))))
(mbe :logic (coerce (append (coerce str1 'list)
(coerce str2 'list))
'string)
:exec (concatenate 'string str1 str2)))
