		Search-engine friendly clone of the ACL2 documentation.

Values

Type-of-value

Leo type of a Leo value.

Signature
(type-of-value value) → type
Arguments: value — Guard (valuep value).
Returns: type — Type (typep type).

In our current formalization, every Leo value has exactly one Leo type. This function associates a type to each value.

Theorem: return-type-of-type-of-value.type

(defthm return-type-of-type-of-value.type
  (b* ((?type (type-of-value value)))
    (typep type))
  :rule-classes :rewrite)

Theorem: return-type-of-type-list-of-value-list.types

(defthm return-type-of-type-list-of-value-list.types
  (b* ((?types (type-list-of-value-list values)))
    (type-listp types))
  :rule-classes :rewrite)

Theorem: len-of-type-list-of-value-list

(defthm len-of-type-list-of-value-list
  (b* ((?types (type-list-of-value-list values)))
    (equal (len types) (len values))))

Theorem: type-of-value-of-value-fix-value

(defthm type-of-value-of-value-fix-value
  (equal (type-of-value (value-fix value))
         (type-of-value value)))

Theorem: type-list-of-value-list-of-value-list-fix-values

(defthm type-list-of-value-list-of-value-list-fix-values
  (equal (type-list-of-value-list (value-list-fix values))
         (type-list-of-value-list values)))

Theorem: type-of-value-value-equiv-congruence-on-value

(defthm type-of-value-value-equiv-congruence-on-value
  (implies (value-equiv value value-equiv)
           (equal (type-of-value value)
                  (type-of-value value-equiv)))
  :rule-classes :congruence)

Theorem: type-list-of-value-list-value-list-equiv-congruence-on-values

(defthm
      type-list-of-value-list-value-list-equiv-congruence-on-values
  (implies (value-list-equiv values values-equiv)
           (equal (type-list-of-value-list values)
                  (type-list-of-value-list values-equiv)))
  :rule-classes :congruence)

Subtopics

Type-list-of-value-list