quote-term-list

(in-package "ACL2")

(define quote-term-list
  ((x true-listp))
  :returns (terms pseudo-term-listp)
  :parents (std/system/term-transformations)
  :short "Lift @(tsee quote-term) to lists."
  (cond ((endp x) nil)
    (t (cons (quote-term (car x)) (quote-term-list (cdr x))))))