Narrowing conversion from
(short-to-char operand) → result
Function:
(defun short-to-char (operand) (declare (xargs :guard (short-valuep operand))) (b* ((x (short-value->int operand))) (char-value (loghead 16 x))))
Theorem:
(defthm char-valuep-of-short-to-char (b* ((result (short-to-char operand))) (char-valuep result)) :rule-classes :rewrite)
Theorem:
(defthm short-to-char-of-short-value-fix-operand (equal (short-to-char (short-value-fix operand)) (short-to-char operand)))
Theorem:
(defthm short-to-char-short-value-equiv-congruence-on-operand (implies (short-value-equiv operand operand-equiv) (equal (short-to-char operand) (short-to-char operand-equiv))) :rule-classes :congruence)