Filtering...

generate-symbol

books/std/util/generate-symbol
other
(in-package "STD")
other
(local (defthm character-listp-of-explode-nonnegative-integer
    (implies (character-listp ans)
      (character-listp (explode-nonnegative-integer n
          print-base
          ans)))))
other
(defn string/symbol/integer-list-p
  (x)
  (cond ((atom x) (null x))
    (t (and (or (stringp (car x))
          (symbolp (car x))
          (integerp (car x)))
        (string/symbol/integer-list-p (cdr x))))))
generate-symbol-fn1function
(defun generate-symbol-fn1
  (lst)
  (declare (xargs :guard (string/symbol/integer-list-p lst)))
  (cond ((atom lst) nil)
    (t (let ((curr (car lst)) (rest (cdr lst)))
        (cond ((stringp curr) (cons curr (generate-symbol-fn1 rest)))
          ((symbolp curr) (cons (symbol-name curr)
              (generate-symbol-fn1 rest)))
          ((integerp curr) (cons (coerce (explode-atom curr 10) 'string)
              (generate-symbol-fn1 rest)))
          (t (er hard
              'generate-symbol-fn1
              "Guards are violated")))))))
generate-symbol-in-package-of-symbolfunction
(defun generate-symbol-in-package-of-symbol
  (string/symbol/decimal-list symbol)
  (declare (xargs :guard (and (string/symbol/integer-list-p string/symbol/decimal-list)
        (symbolp symbol))))
  (intern-in-package-of-symbol (string-append-lst (generate-symbol-fn1 string/symbol/decimal-list))
    symbol))