Generic stub for a character type recognizer.
This is the basis of the generic theory that defchar instantiates. Typically this is standing in for a function that recognizes some particular set of characters, say digits. The only constraints are that:
Definition:
(encapsulate (((vl-ctype-p *) => *)) (local (value-triple :elided)) (defrule vl-ctype-p-of-nil (not (vl-ctype-p nil))) (defrule booleanp-of-vl-ctype-p (booleanp (vl-ctype-p x)) :rule-classes :type-prescription))
Theorem:
(defthm vl-ctype-p-of-nil (not (vl-ctype-p nil)))
Theorem:
(defthm booleanp-of-vl-ctype-p (booleanp (vl-ctype-p x)) :rule-classes :type-prescription)