Pad a string with spaces on the left.
(lpadstr x len) extends the string
(lpadstr "foo" 5) --> " foo"
This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add
If no new spaces are needed,
(defun lpadstr (x len) (declare (xargs :guard (and (stringp x) (natp len))) (type string x) (type integer len)) (mbe :logic (implode (lpadchars (explode x) len)) :exec (let* ((x-len (length x)) (diff (- len x-len))) (if (< 0 diff) (implode (make-list-ac diff #\Space (explode x))) x))))
(defthm len-of-explode-of-lpadstr (implies (force (stringp x)) (equal (len (explode (lpadstr x len))) (max (length x) (nfix len)))))
(defthm streqv-implies-equal-lpadstr-1 (implies (streqv x x-equiv) (equal (lpadstr x len) (lpadstr x-equiv len))) :rule-classes (:congruence))