Annotate an ACL2 variable with a non-empty list of types.
(atj-type-annotate-var var types) → annotated-var
As mentioned in atj-pre-translation-type-annotation,
we systematically add type information to each ACL2 variable.
We do so by adding
The result of this function is never the symbol
Function:
(defun atj-type-annotate-var (var types) (declare (xargs :guard (and (symbolp var) (atj-type-listp types)))) (declare (xargs :guard (consp types))) (let ((__function__ 'atj-type-annotate-var)) (declare (ignorable __function__)) (packn-pos (list "[" (atj-types-id types) "]" var) var)))
Theorem:
(defthm symbolp-of-atj-type-annotate-var (b* ((annotated-var (atj-type-annotate-var var types))) (symbolp annotated-var)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-annotate-var-not-nil (implies (symbolp var) (not (equal (atj-type-annotate-var var types) nil))) :rule-classes :type-prescription)