		Search-engine friendly clone of the ACL2 documentation.

Operations

Lt-values

Apply < to values [C17:6.5.8/2] [C17:6.5.8/3] [C17:6.5.8/6].

Signature
(lt-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (value-resultp resval).

It is an error if the values are not real; we do not support comparison of pointers yet.

Definitions and Theorems

Function: lt-values

(defun lt-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (let ((__function__ 'lt-values))
    (declare (ignorable __function__))
    (if (and (value-realp val1)
             (value-realp val2))
        (lt-real-values val1 val2)
      (error (list :lt-mistype :required
                   :real :real :supplied (value-fix val1)
                   (value-fix val2))))))

Theorem: value-resultp-of-lt-values

(defthm value-resultp-of-lt-values
  (b* ((resval (lt-values val1 val2)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: lt-values-of-value-fix-val1

(defthm lt-values-of-value-fix-val1
  (equal (lt-values (value-fix val1) val2)
         (lt-values val1 val2)))

Theorem: lt-values-value-equiv-congruence-on-val1

(defthm lt-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (lt-values val1 val2)
                  (lt-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: lt-values-of-value-fix-val2

(defthm lt-values-of-value-fix-val2
  (equal (lt-values val1 (value-fix val2))
         (lt-values val1 val2)))

Theorem: lt-values-value-equiv-congruence-on-val2

(defthm lt-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (lt-values val1 val2)
                  (lt-values val1 val2-equiv)))
  :rule-classes :congruence)