		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appcond-name-from-parts

Create the name (keyword) of an applicability condition from its parts.

Signature
(casesplit-gen-appcond-name-from-parts prefix k suffix) → name
Arguments: prefix — Guard (stringp prefix).; k — Guard (natp k).; suffix — Guard (stringp suffix).
Returns: name — A keyword.
Type (symbolp name).

All the applicability condition names consist of a prefix (thm or cond or new) a number k, and a suffix (-hyp or -guard).

Definitions and Theorems

Function: casesplit-gen-appcond-name-from-parts

(defun casesplit-gen-appcond-name-from-parts (prefix k suffix)
  (declare (xargs :guard (and (stringp prefix)
                              (natp k)
                              (stringp suffix))))
  (let ((__function__ 'casesplit-gen-appcond-name-from-parts))
    (declare (ignorable __function__))
    (intern (str::cat prefix (str::nat-to-dec-string k)
                      suffix)
            "KEYWORD")))

Theorem: symbolp-of-casesplit-gen-appcond-name-from-parts

(defthm symbolp-of-casesplit-gen-appcond-name-from-parts
  (b*
    ((name (casesplit-gen-appcond-name-from-parts prefix k suffix)))
    (symbolp name))
  :rule-classes :rewrite)