strings - ACL2 Book

other

(in-package "ACL2")

n-string-appendmacro

(defmacro n-string-append
  (&rest strings)
  `(concatenate 'string ,@STRINGS))

newline-stringfunction

(defun newline-string
  nil
  (declare (xargs :guard t))
  "
")