• 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
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Litp

Lit-fix

Basic fixing function for literals.

Signature

(lit-fix x) → x-fix

Arguments

x — Guard (litp x).

Returns

x-fix — Type (litp x-fix).

Definitions and Theorems

Function: lit-fix$inline

(defun lit-fix$inline (x)
       (declare (xargs :guard (litp x)))
       (let ((__function__ 'lit-fix))
            (declare (ignorable __function__))
            (lnfix x)))

Theorem: litp-of-lit-fix

(defthm litp-of-lit-fix
        (b* ((x-fix (lit-fix$inline x)))
            (litp x-fix))
        :rule-classes :type-prescription)

Theorem: lit-fix-of-lit

(defthm lit-fix-of-lit
        (implies (litp x)
                 (equal (lit-fix x) x)))