Return the type sum that defines a type, if any.
(get-type-sum type tops) → tprod
Function:
(defun get-type-sum (type tops) (declare (xargs :guard (and (typep type) (toplevel-listp tops)))) (let ((__function__ 'get-type-sum)) (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 nil :sum definer.get :subset nil)))))
Theorem:
(defthm maybe-type-sump-of-get-type-sum (b* ((tprod (get-type-sum type tops))) (maybe-type-sump tprod)) :rule-classes :rewrite)
Theorem:
(defthm get-type-sum-of-type-fix-type (equal (get-type-sum (type-fix type) tops) (get-type-sum type tops)))
Theorem:
(defthm get-type-sum-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (get-type-sum type tops) (get-type-sum type-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm get-type-sum-of-toplevel-list-fix-tops (equal (get-type-sum type (toplevel-list-fix tops)) (get-type-sum type tops)))
Theorem:
(defthm get-type-sum-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (get-type-sum type tops) (get-type-sum type tops-equiv))) :rule-classes :congruence)