Return the type product that defines a type, if any.
(get-type-product type tops) → tprod
Function:
(defun get-type-product (type tops) (declare (xargs :guard (and (typep type) (toplevel-listp tops)))) (let ((__function__ 'get-type-product)) (declare (ignorable __function__)) (type-case type :boolean nil :character nil :string nil :integer nil :set nil :sequence nil :map nil :option nil :defined (b* ((typedef (get-type-definition type.name tops)) ((when (not typedef)) nil) (definer (type-definition->body typedef)) ((when (not definer)) nil)) (type-definer-case definer :product definer.get :sum nil :subset nil)))))
Theorem:
(defthm maybe-type-productp-of-get-type-product (b* ((tprod (get-type-product type tops))) (maybe-type-productp tprod)) :rule-classes :rewrite)
Theorem:
(defthm get-type-product-of-type-fix-type (equal (get-type-product (type-fix type) tops) (get-type-product type tops)))
Theorem:
(defthm get-type-product-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (get-type-product type tops) (get-type-product type-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm get-type-product-of-toplevel-list-fix-tops (equal (get-type-product type (toplevel-list-fix tops)) (get-type-product type tops)))
Theorem:
(defthm get-type-product-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (get-type-product type tops) (get-type-product type tops-equiv))) :rule-classes :congruence)