Logrpl
Logical replace. (logrpl size i j) replaces the size
low-order bits of j with the size low-order bits of i.
- Signature
(logrpl size i j) → int
- Arguments
- size — Guard (and (integerp size) (<= 0 size)).
- i — Guard (integerp i).
- j — Guard (integerp j).
- Returns
- int — Type (integerp int).
logrpl is a specification for the result of storing short
values into long words, i.e., the short value simply replaces the head of the
long word.
This function is equivalent to (WRB i (BSP size 0) j).
Definitions and Theorems
Function: logrpl
(defun logrpl (size i j)
(declare (xargs :guard (and (and (integerp size) (<= 0 size))
(integerp i)
(integerp j))))
(let ((__function__ 'logrpl))
(declare (ignorable __function__))
(logapp size i (logtail size j))))
Theorem: logrpl-type
(defthm logrpl-type
(b* ((int (logrpl size i j)))
(integerp int))
:rule-classes :type-prescription)
Subtopics
- Ihs/logrpl-lemmas
- Lemmas about logrpl from the logops-lemmas book.
