• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
      • Symbol-symbol-alistp
      • String-string-alistp
      • Symbol-string-alistp
      • Symbol-pseudoeventform-alistp
      • Symbol-pseudoterm-alistp
      • String-symbollist-alistp
      • Symbol-pos-alistp
      • Cons-pos-alistp
      • Symbol-symbollist-alistp
      • Symbol-truelist-alistp
      • Keyword-symbol-alistp
      • String-stringlist-alistp
      • Keyword-truelist-alistp
      • Symbol-nat-alistp
      • String-symbol-alistp
      • Keyword-to-keyword-value-list-alistp
      • Std/typed-alists/symbol-alistp
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/typed-alists

Keyword-to-keyword-value-list-alistp

Recognize alists from keywords to keyword-value lists.

A keyword-value list is a true list of even length whose even-position elements are keywords; see keyword-value-listp.

Definitions and Theorems

Function: keyword-to-keyword-value-list-alistp

(defun keyword-to-keyword-value-list-alistp (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
        (t (and (consp (car x))
                (keywordp (car (car x)))
                (keyword-value-listp (cdr (car x)))
                (keyword-to-keyword-value-list-alistp (cdr x))))))