		Search-engine friendly clone of the ACL2 documentation.

Source-character-set

Ascii-to-source-char-number

Number of the basic source character corresponding to an ASCII character.

Signature
(ascii-to-source-char-number x) → number
Arguments: x — Guard (ascii-basic-source-charp x).
Returns: number — Type (natp number).

Definitions and Theorems

Function: ascii-to-source-char-number

(defun ascii-to-source-char-number (x)
  (declare (xargs :guard (ascii-basic-source-charp x)))
  (source-char-to-number (ascii-to-source-char x)))

Theorem: natp-of-ascii-to-source-char-number

(defthm natp-of-ascii-to-source-char-number
  (b* ((number (ascii-to-source-char-number x)))
    (natp number))
  :rule-classes :type-prescription)

Theorem: ascii-to-source-char-number-of-ascii-basic-source-char-fix-x

(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: ascii-to-source-char-number-ascii-basic-source-char-equiv-congruence-on-x

(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)