		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-coretypename-p

Basic kinds of data types.

Our core types basically correspond to the following small subset of the valid data_types:

data_type_or_void ::= data_type | 'void'
data_type ::=
    integer_vector_type [signing] { packed_dimension }
  | integer_atom_type [signing]
  | non_integer_type
  | 'string'
  | 'chandle'
  | 'event'
  | <non core types >

We include void here only because it's convenient to do so.

This is an ordinary defenum.

Function: vl-coretypename-p

(defun vl-coretypename-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-logic)
      (eq x ':vl-reg)
      (eq x ':vl-bit)
      (eq x ':vl-byte)
      (eq x ':vl-shortint)
      (eq x ':vl-int)
      (eq x ':vl-longint)
      (eq x ':vl-integer)
      (eq x ':vl-time)
      (eq x ':vl-shortreal)
      (eq x ':vl-real)
      (eq x ':vl-realtime)
      (eq x ':vl-string)
      (eq x ':vl-chandle)
      (eq x ':vl-event)
      (eq x ':vl-void)))

Theorem: type-when-vl-coretypename-p

(defthm type-when-vl-coretypename-p
  (implies (vl-coretypename-p x)
           (if (symbolp x)
               (if (not (equal x 't))
                   (not (equal x 'nil))
                 'nil)
             'nil))
  :rule-classes :compound-recognizer)