		Search-engine friendly clone of the ACL2 documentation.

Valid-designor-list

Validate a list of zero or more designators.

Signature
(valid-designor-list designors target-type table ienv) → (mv erp new-designors new-target-type return-types new-table)
Arguments: designors — Guard (designor-listp designors).; target-type — Guard (typep target-type).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-designors — Type (designor-listp new-designors).; new-target-type — Type (typep new-target-type).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The target type passed as argument is the current type that the designators must be applicable to. The target type returned as result is the type resulting from the application of the designators.

Definitions and Theorems

Theorem: valid-designor-list.new-target-type-not-function

(defthm valid-designor-list.new-target-type-not-function
  (b* (((mv acl2::?erp
            ?new-designors ?new-target-type
            ?return-types ?new-table)
        (valid-designor-list designors target-type table ienv)))
    (implies (not erp)
             (not (equal (type-kind new-target-type)
                         :function)))))

Theorem: valid-designor-list.new-target-type-not-void

(defthm valid-designor-list.new-target-type-not-void
  (b* (((mv acl2::?erp
            ?new-designors ?new-target-type
            ?return-types ?new-table)
        (valid-designor-list designors target-type table ienv)))
    (implies (not erp)
             (not (equal (type-kind new-target-type)
                         :void)))))