• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
        • Alist-keys
        • Remove-assocs
        • Alist-vals
        • Alist-map-vals
        • Alist-map-keys
        • Std/alists/strip-cdrs
        • Hons-rassoc-equal
        • Std/alists/hons-assoc-equal
        • Std/alists/strip-cars
        • Fal-find-any
        • Fal-extract
        • Std/alists/abstract
          • Keyval-alist-p
          • Valtype-p
          • Keytype-p
          • Def-alistp-rule
          • Fal-extract-vals
          • Fal-all-boundp
          • Std/alists/alistp
          • Append-alist-vals
          • Append-alist-keys
          • Alist-equiv
          • Hons-remove-assoc
          • Std/alists/pairlis$
          • Worth-hashing
          • Alists-agree
          • Sub-alistp
          • Alist-fix
          • Std/alists/remove-assoc-equal
          • Std/alists/assoc-equal
        • Obags
        • Std/util
        • Std/strings
        • Std/io
        • Std/osets
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Std/alists/abstract

    Def-alistp-rule

    Define a theorem and save it in a table, denoting that it is a rule about keyval-alistp.