• Top
  • Documentation
  • Books
  • 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
          • Lit-list
          • Maybe-litp
            • Maybe-lit-fix
          • Lit-fix
          • Lit-list-list
        • 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
  • Math
  • Testing-utilities

• Litp

Maybe-litp

Recognizer for lits and nil.

This is like an option type; when x satisfies maybe-litp, then either it is a litp or nothing.

Definitions and Theorems

Function: maybe-litp$inline

(defun maybe-litp$inline (x)
  (declare (xargs :guard t))
  (or (not x) (litp x)))

Theorem: maybe-litp-compound-recognizer

(defthm maybe-litp-compound-recognizer
  (equal (maybe-litp x)
         (or (not x) (litp x)))
  :rule-classes :compound-recognizer)

Subtopics

Maybe-lit-fix

(maybe-lit-fix x) is the identity for maybe-litps, or coerces any non-litp to nil.