Default ATJ function type information for a function.
(atj-function-type-info-default fn wrld) → fn-info
This is used when a function has no entry in the table.
It consists of a primary function type of all
To calculate the output types,
we need the number of results returned by
Function:
(defun atj-function-type-info-default (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'atj-function-type-info-default)) (declare (ignorable __function__)) (b* ((number-of-inputs (arity+ fn wrld)) (number-of-outputs (atj-number-of-results fn wrld))) (make-atj-function-type-info :main (make-atj-function-type :inputs (repeat number-of-inputs (atj-type-acl2 (atj-atype-value))) :outputs (repeat number-of-outputs (atj-type-acl2 (atj-atype-value))) :arrays (repeat number-of-outputs nil)) :others nil))))
Theorem:
(defthm atj-function-type-info-p-of-atj-function-type-info-default (b* ((fn-info (atj-function-type-info-default fn wrld))) (atj-function-type-info-p fn-info)) :rule-classes :rewrite)