• 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
        • 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

• Litp

Lit-list-list

List of lit-lists

This is an ordinary fty::deflist.

Subtopics

Lit-list-list-fix

(lit-list-list-fix x) is a usual ACL2::fty list fixing function.

Lit-list-list-equiv

Basic equivalence relation for lit-list-list structures.

Lit-list-listp

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