		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-const

Validate a constant.

Signature
(valid-const const table ienv) → (mv erp type)
Arguments: const — Guard (constp const).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: type — Type (typep type).

If validation is successful, we return the type of the constant.

Definitions and Theorems

Function: valid-const

(defun valid-const (const table ienv)
  (declare (xargs :guard (and (constp const)
                              (valid-tablep table)
                              (ienvp ienv))))
  (let ((__function__ 'valid-const))
    (declare (ignorable __function__))
    (const-case const
                :int (valid-iconst const.unwrap ienv)
                :float (retok (valid-fconst const.unwrap))
                :enum (valid-enum-const const.unwrap table)
                :char (valid-cconst const.unwrap))))

Theorem: typep-of-valid-const.type

(defthm typep-of-valid-const.type
  (b* (((mv acl2::?erp ?type)
        (valid-const const table ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-const-of-const-fix-const

(defthm valid-const-of-const-fix-const
  (equal (valid-const (const-fix const)
                      table ienv)
         (valid-const const table ienv)))

Theorem: valid-const-const-equiv-congruence-on-const

(defthm valid-const-const-equiv-congruence-on-const
  (implies (const-equiv const const-equiv)
           (equal (valid-const const table ienv)
                  (valid-const const-equiv table ienv)))
  :rule-classes :congruence)

Theorem: valid-const-of-valid-table-fix-table

(defthm valid-const-of-valid-table-fix-table
  (equal (valid-const const (valid-table-fix table)
                      ienv)
         (valid-const const table ienv)))

Theorem: valid-const-valid-table-equiv-congruence-on-table

(defthm valid-const-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-const const table ienv)
                  (valid-const const table-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-const-of-ienv-fix-ienv

(defthm valid-const-of-ienv-fix-ienv
  (equal (valid-const const table (ienv-fix ienv))
         (valid-const const table ienv)))

Theorem: valid-const-ienv-equiv-congruence-on-ienv

(defthm valid-const-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-const const table ienv)
                  (valid-const const table ienv-equiv)))
  :rule-classes :congruence)