Convert from type
Function:
(defun schar-from-slong (x) (declare (xargs :guard (slongp x))) (declare (xargs :guard (schar-from-slong-okp x))) (let ((__function__ 'schar-from-slong)) (declare (ignorable __function__)) (schar-from-integer (integer-from-slong x))))
Theorem:
(defthm scharp-of-schar-from-slong (b* ((result (schar-from-slong x))) (scharp result)) :rule-classes :rewrite)
Theorem:
(defthm schar-from-slong-of-slong-fix-x (equal (schar-from-slong (slong-fix x)) (schar-from-slong x)))
Theorem:
(defthm schar-from-slong-slong-equiv-congruence-on-x (implies (slong-equiv x x-equiv) (equal (schar-from-slong x) (schar-from-slong x-equiv))) :rule-classes :congruence)