• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
        • Alist-keys
        • Remove-assocs
        • Alist-vals
        • Alist-map-vals
        • Std/alists/strip-cdrs
        • Hons-rassoc-equal
        • Alist-map-keys
        • Std/alists/hons-assoc-equal
        • Fal-extract
        • Std/alists/strip-cars
        • Fal-find-any
        • Fal-extract-vals
        • Std/alists/abstract
          • Keyval-alist-p
          • Valtype-p
            • Keytype-p
            • Def-alistp-rule
          • Fal-all-boundp
          • Std/alists/alistp
          • Append-alist-vals
          • Append-alist-keys
          • Alist-equiv
          • Hons-remove-assoc
          • Std/alists/pairlis$
          • Alists-agree
          • Worth-hashing
          • Sub-alistp
          • Alist-fix
          • Std/alists/remove-assoc-equal
          • Std/alists/assoc-equal
        • Obags
        • Std/util
        • Std/strings
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • 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/alists/abstract

    Valtype-p

    Generic typed list valtype recognizer.

    Definitions and Theorems

    Theorem: non-valtype-p-def

    (defthm non-valtype-p-def
            (iff (non-valtype-p x)
                 (not (valtype-p x))))