		Search-engine friendly clone of the ACL2 documentation.

boolean-literals

The Java boolean literals, as ACL2 strings.

Definition: *boolean-literals*

(defconst *boolean-literals*
  (list "true" "false"))

Theorem: ascii-listp-of-boolean-literals

(defthm ascii-listp-of-boolean-literals
  (implies (member-equal literal *boolean-literals*)
           (ascii-listp (string=>unicode literal))))