		Search-engine friendly clone of the ACL2 documentation.

Stv2c-c-symbol-name

Stv2c-tailchar-p

Signature
(stv2c-tailchar-p x) → *
Arguments: x — Guard (characterp x).

Definitions and Theorems

Function: stv2c-tailchar-p

(defun stv2c-tailchar-p (x)
       (declare (xargs :guard (characterp x)))
       (let ((__function__ 'stv2c-tailchar-p))
            (declare (ignorable __function__))
            (or (str::dec-digit-char-p x)
                (str::down-alpha-p x)
                (str::up-alpha-p x)
                (eql x #\_))))