		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-get-fn-method-name

Retrieve the Java method name for an ACL2 function name from the mapping, ensuring that the name is present.

Signature
(atj-get-fn-method-name fn fn-method-names) → method
Arguments: fn — Guard (symbolp fn).; fn-method-names — Guard (symbol-string-alistp fn-method-names).
Returns: method — Type (stringp method), given (symbol-string-alistp fn-method-names).

This function causes an error if the function name is not in the alist, but it should always be called with arguments that do not result in the error. In other words, the error is never expected to actually happen.

Definitions and Theorems

Function: atj-get-fn-method-name

(defun atj-get-fn-method-name (fn fn-method-names)
  (declare
       (xargs :guard (and (symbolp fn)
                          (symbol-string-alistp fn-method-names))))
  (let ((__function__ 'atj-get-fn-method-name))
    (declare (ignorable __function__))
    (b* ((pair (assoc-equal fn fn-method-names))
         ((unless (consp pair))
          (raise "Internal error: no method name for function ~x0."
                 fn)
          ""))
      (cdr pair))))

Theorem: stringp-of-atj-get-fn-method-name

(defthm stringp-of-atj-get-fn-method-name
 (implies (symbol-string-alistp fn-method-names)
          (b* ((method (atj-get-fn-method-name fn fn-method-names)))
            (stringp method)))
 :rule-classes :rewrite)