		Search-engine friendly clone of the ACL2 documentation.

Ordering-operations

Op-lt

Leo less-than operation.

Signature
(op-lt left right) → result
Arguments: left — Guard (valuep left).; right — Guard (valuep right).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-lt

(defun op-lt (left right)
  (declare (xargs :guard (and (valuep left) (valuep right))))
  (let ((__function__ 'op-lt))
    (declare (ignorable __function__))
    (cond ((and (value-case left :u8)
                (value-case right :u8))
           (value-bool (< (value-u8->get left)
                          (value-u8->get right))))
          ((and (value-case left :u16)
                (value-case right :u16))
           (value-bool (< (value-u16->get left)
                          (value-u16->get right))))
          ((and (value-case left :u32)
                (value-case right :u32))
           (value-bool (< (value-u32->get left)
                          (value-u32->get right))))
          ((and (value-case left :u64)
                (value-case right :u64))
           (value-bool (< (value-u64->get left)
                          (value-u64->get right))))
          ((and (value-case left :u128)
                (value-case right :u128))
           (value-bool (< (value-u128->get left)
                          (value-u128->get right))))
          ((and (value-case left :i8)
                (value-case right :i8))
           (value-bool (< (value-i8->get left)
                          (value-i8->get right))))
          ((and (value-case left :i16)
                (value-case right :i16))
           (value-bool (< (value-i16->get left)
                          (value-i16->get right))))
          ((and (value-case left :i32)
                (value-case right :i32))
           (value-bool (< (value-i32->get left)
                          (value-i32->get right))))
          ((and (value-case left :i64)
                (value-case right :i64))
           (value-bool (< (value-i64->get left)
                          (value-i64->get right))))
          ((and (value-case left :i128)
                (value-case right :i128))
           (value-bool (< (value-i128->get left)
                          (value-i128->get right))))
          ((and (value-case left :field)
                (value-case right :field))
           (value-bool (< (value-field->get left)
                          (value-field->get right))))
          ((and (value-case left :scalar)
                (value-case right :scalar))
           (value-bool (< (value-scalar->get left)
                          (value-scalar->get right))))
          (t (reserrf (list :op-lt (value-fix left)
                            (value-fix right)))))))

Theorem: value-resultp-of-op-lt

(defthm value-resultp-of-op-lt
  (b* ((result (op-lt left right)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-lt-of-value-fix-left

(defthm op-lt-of-value-fix-left
  (equal (op-lt (value-fix left) right)
         (op-lt left right)))

Theorem: op-lt-value-equiv-congruence-on-left

(defthm op-lt-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-lt left right)
                  (op-lt left-equiv right)))
  :rule-classes :congruence)

Theorem: op-lt-of-value-fix-right

(defthm op-lt-of-value-fix-right
  (equal (op-lt left (value-fix right))
         (op-lt left right)))

Theorem: op-lt-value-equiv-congruence-on-right

(defthm op-lt-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-lt left right)
                  (op-lt left right-equiv)))
  :rule-classes :congruence)