		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Eval-const

Evaluate a constant.

Signature
(eval-const c) → val
Arguments: c — Guard (constp c).
Returns: val — Type (value-resultp val).

We only support the evaluation of integer constants for now.

Definitions and Theorems

Function: eval-const

(defun eval-const (c)
  (declare (xargs :guard (constp c)))
  (let ((__function__ 'eval-const))
    (declare (ignorable __function__))
    (const-case c
                :int (eval-iconst c.get)
                :float (error :exec-const-float)
                :enum (error :exec-const-enum)
                :char (error :exec-const-char))))

Theorem: value-resultp-of-eval-const

(defthm value-resultp-of-eval-const
  (b* ((val (eval-const c)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-const-of-const-fix-c

(defthm eval-const-of-const-fix-c
  (equal (eval-const (const-fix c))
         (eval-const c)))

Theorem: eval-const-const-equiv-congruence-on-c

(defthm eval-const-const-equiv-congruence-on-c
  (implies (const-equiv c c-equiv)
           (equal (eval-const c)
                  (eval-const c-equiv)))
  :rule-classes :congruence)