		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Tyspecseq-to-type

Map a type specifier sequence from the language formalization to the corresponding type.

Signature
(tyspecseq-to-type tyspecseq) → (mv okp type)
Arguments: tyspecseq — Guard (c::tyspecseqp tyspecseq).
Returns: okp — Type (booleanp okp).; type — Type (c::typep type).

For now we only allow certain types.

Definitions and Theorems

Function: tyspecseq-to-type

(defun tyspecseq-to-type (tyspecseq)
  (declare (xargs :guard (c::tyspecseqp tyspecseq)))
  (let ((__function__ 'tyspecseq-to-type))
    (declare (ignorable __function__))
    (c::tyspecseq-case tyspecseq
                       :uchar (mv t (c::type-uchar))
                       :schar (mv t (c::type-schar))
                       :ushort (mv t (c::type-ushort))
                       :sshort (mv t (c::type-sshort))
                       :uint (mv t (c::type-uint))
                       :sint (mv t (c::type-sint))
                       :ulong (mv t (c::type-ulong))
                       :slong (mv t (c::type-slong))
                       :ullong (mv t (c::type-ullong))
                       :sllong (mv t (c::type-sllong))
                       :otherwise (mv nil (c::type-void)))))

Theorem: booleanp-of-tyspecseq-to-type.okp

(defthm booleanp-of-tyspecseq-to-type.okp
  (b* (((mv ?okp common-lisp::?type)
        (tyspecseq-to-type tyspecseq)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: typep-of-tyspecseq-to-type.type

(defthm typep-of-tyspecseq-to-type.type
  (b* (((mv ?okp common-lisp::?type)
        (tyspecseq-to-type tyspecseq)))
    (c::typep type))
  :rule-classes :rewrite)

Theorem: tyspecseq-to-type-of-tyspecseq-fix-tyspecseq

(defthm tyspecseq-to-type-of-tyspecseq-fix-tyspecseq
  (equal (tyspecseq-to-type (c::tyspecseq-fix tyspecseq))
         (tyspecseq-to-type tyspecseq)))

Theorem: tyspecseq-to-type-tyspecseq-equiv-congruence-on-tyspecseq

(defthm tyspecseq-to-type-tyspecseq-equiv-congruence-on-tyspecseq
  (implies (c::tyspecseq-equiv tyspecseq tyspecseq-equiv)
           (equal (tyspecseq-to-type tyspecseq)
                  (tyspecseq-to-type tyspecseq-equiv)))
  :rule-classes :congruence)