Name of the Java method that builds a deeply embedded ACL2 function definition.
We generate a private static method for each deeply embedded ACL2 function definition to build. This function generates the name of this method, which is distinct from all the other methods generated for the same class.
Function:
(defun atj-gen-deep-fndef-method-name (fn) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'atj-gen-deep-fndef-method-name)) (declare (ignorable __function__)) (str::cat "addFunctionDef_" (implode (atj-chars-to-jchars-id (explode (symbol-package-name fn)) nil :dash nil)) "$$$" (implode (atj-chars-to-jchars-id (explode (symbol-name fn)) nil :dash t)))))
Theorem:
(defthm stringp-of-atj-gen-deep-fndef-method-name (b* ((method-name (atj-gen-deep-fndef-method-name fn))) (stringp method-name)) :rule-classes :rewrite)