		Search-engine friendly clone of the ACL2 documentation.

C-char-char

C-char-char->code

Get the code field from a c-char-char.

Signature
(c-char-char->code x) → code
Arguments: x — Guard (c-char-p x).
Returns: code — Type (natp code).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: c-char-char->code$inline

(defun c-char-char->code$inline (x)
  (declare (xargs :guard (c-char-p x)))
  (declare (xargs :guard (equal (c-char-kind x) :char)))
  (mbe :logic
       (b* ((x (and (equal (c-char-kind x) :char) x)))
         (nfix (cdr x)))
       :exec (cdr x)))

Theorem: natp-of-c-char-char->code

(defthm natp-of-c-char-char->code
  (b* ((code (c-char-char->code$inline x)))
    (natp code))
  :rule-classes :rewrite)

Theorem: c-char-char->code$inline-of-c-char-fix-x

(defthm c-char-char->code$inline-of-c-char-fix-x
  (equal (c-char-char->code$inline (c-char-fix x))
         (c-char-char->code$inline x)))

Theorem: c-char-char->code$inline-c-char-equiv-congruence-on-x

(defthm c-char-char->code$inline-c-char-equiv-congruence-on-x
  (implies (c-char-equiv x x-equiv)
           (equal (c-char-char->code$inline x)
                  (c-char-char->code$inline x-equiv)))
  :rule-classes :congruence)

Theorem: c-char-char->code-when-wrong-kind

(defthm c-char-char->code-when-wrong-kind
  (implies (not (equal (c-char-kind x) :char))
           (equal (c-char-char->code x)
                  (nfix nil))))