• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/system
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
        • Two-nats-measure
        • Impossible
        • Nat-list-measure
        • Bytep
        • Maybe-posp
        • Nibblep
        • Mbt$
        • Organize-symbols-by-pkg
        • Organize-symbols-by-name
        • Good-valuep
        • Lnfix
        • Streqv
        • Chareqv
        • Symbol-package-name-non-cl
        • Std/basic-extensions
        • Arith-equivs
        • Induction-schemes
        • Maybe-integerp
        • Char-fix
        • Symbol-package-name-lst
        • Pos-fix
        • Maybe-bitp
        • Good-pseudo-termp
        • Str-fix
        • Maybe-string-fix
        • Lifix
        • Bfix
        • Std/basic/if*
        • Impliez
        • Tuplep
        • Std/basic/symbol-name-lst
          • Std/basic/intern-in-package-of-symbol
          • Lbfix
          • True
          • Std/basic/member-symbol-name
          • False
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Std/basic
    • Symbol-name-lst

    Std/basic/symbol-name-lst

    Theorems about symbol-name-lst in the Std/basic library.

    Definitions and Theorems

    Theorem: string-listp-of-symbol-name-lst

    (defthm string-listp-of-symbol-name-lst
            (string-listp (symbol-name-lst syms)))

    Theorem: len-of-symbol-name-lst

    (defthm len-of-symbol-name-lst
            (equal (len (symbol-name-lst syms))
                   (len syms)))