Included Books
other
(in-package "ACL2")
include-book
(include-book "std/util/define" :dir :system)
other
(define quote-term (x) :returns (term pseudo-termp) :parents (std/system/term-transformations) :short "Build a quoted constant term with the given value." (list 'quote x) /// (defret quotep-of-quote-term (quotep (quote-term x))))