Number of the basic source character corresponding to an ASCII character.
(ascii-to-source-char-number x) → number
Function:
(defun ascii-to-source-char-number (x) (declare (xargs :guard (ascii-basic-source-charp x))) (let ((__function__ 'ascii-to-source-char-number)) (declare (ignorable __function__)) (source-char-to-number (ascii-to-source-char x))))
Theorem:
(defthm natp-of-ascii-to-source-char-number (b* ((number (ascii-to-source-char-number x))) (natp number)) :rule-classes :type-prescription)
Theorem:
(defthm ascii-to-source-char-number-of-ascii-basic-source-char-fix-x (equal (ascii-to-source-char-number (ascii-basic-source-char-fix x)) (ascii-to-source-char-number x)))
Theorem:
(defthm ascii-to-source-char-number-ascii-basic-source-char-equiv-congruence-on-x (implies (ascii-basic-source-char-equiv x x-equiv) (equal (ascii-to-source-char-number x) (ascii-to-source-char-number x-equiv))) :rule-classes :congruence)