• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
        • Sat-solver-options
        • Config-p
        • Logical-story
        • Dimacs
        • Gather-benchmarks
        • Cnf
          • Litp
            • Lit-negate-cond
            • Lit-negate
            • Make-lit
            • Lit-equiv
            • Lit->var
            • Lit->neg
            • Maybe-litp
            • Lit-list
            • Lit-fix
            • Lit-list-list
              • Lit-list-list-fix
              • Lit-list-list-equiv
              • Lit-list-listp
                • Lit-list-listp-basics
          • Varp
          • Env$
          • Eval-formula
          • Max-index-formula
          • Max-index-clause
          • Formula-indices
          • Clause-indices
        • Satlink-extra-hook
        • Sat
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Lit-list-list

Lit-list-listp

(lit-list-listp x) recognizes lists where every element satisfies lit-listp.

Signature
(lit-list-listp x) → *

This is an ordinary deflist. It is "strict" in that it requires x to be a "properly" nil-terminated list.

Subtopics

Lit-list-listp-basics
Basic theorems about lit-list-listp, generated by deflist.