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