ATJ type conversion function names used to annotate ACL2 terms.
(atj-type-conv src-types dst-types) → name
As mentioned in atj-pre-translation-type-annotation,
each ACL2 term is wrapped with a function named
These function names are all in the
Function:
(defun atj-type-conv (src-types dst-types) (declare (xargs :guard (and (atj-type-listp src-types) (atj-type-listp dst-types)))) (declare (xargs :guard (and (consp src-types) (consp dst-types)))) (let ((__function__ 'atj-type-conv)) (declare (ignorable __function__)) (intern$ (str::cat "[" (atj-types-id src-types) ">" (atj-types-id dst-types) "]") "JAVA")))
Theorem:
(defthm symbolp-of-atj-type-conv (b* ((name (atj-type-conv src-types dst-types))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-conv-of-atj-type-list-fix-src-types (equal (atj-type-conv (atj-type-list-fix src-types) dst-types) (atj-type-conv src-types dst-types)))
Theorem:
(defthm atj-type-conv-atj-type-list-equiv-congruence-on-src-types (implies (atj-type-list-equiv src-types src-types-equiv) (equal (atj-type-conv src-types dst-types) (atj-type-conv src-types-equiv dst-types))) :rule-classes :congruence)
Theorem:
(defthm atj-type-conv-of-atj-type-list-fix-dst-types (equal (atj-type-conv src-types (atj-type-list-fix dst-types)) (atj-type-conv src-types dst-types)))
Theorem:
(defthm atj-type-conv-atj-type-list-equiv-congruence-on-dst-types (implies (atj-type-list-equiv dst-types dst-types-equiv) (equal (atj-type-conv src-types dst-types) (atj-type-conv src-types dst-types-equiv))) :rule-classes :congruence)