Filtering...

member-symbol-name

books/std/basic/member-symbol-name

Included Books

constructors
other
(in-package "ACL2")
include-book
(include-book "xdoc/constructors" :dir :system)
other
(defsection std/basic/member-symbol-name
  :parents (std/basic)
  :short "Theorems about the built-in function @('member-symbol-name')."
  (defthm member-symbol-name-when-atom
    (implies (atom symbols)
      (not (member-symbol-name string symbols)))
    :hints (("Goal" :in-theory (enable member-symbol-name))))
  (in-theory (disable member-symbol-name)))