		Search-engine friendly clone of the ACL2 documentation.

Std/system/constant-queries

Constant-value

Return the value of a named constant.

Signature
(constant-value const wrld) → val
Arguments: const — Guard (symbolp const).; wrld — Guard (plist-worldp wrld).

An error occurs if the symbol is not a named constant in the world.

If it is a named constant in the world, we retrieve its const property, which is the quoted value, and we unquote it and return it.

Definitions and Theorems

Function: constant-value

(defun constant-value (const wrld)
 (declare (xargs :guard (and (symbolp const)
                             (plist-worldp wrld))))
 (let ((__function__ 'constant-value))
  (declare (ignorable __function__))
  (b*
   (((unless (constant-symbolp const wrld))
     (raise "~x0 is not a named constant." const))
    (qval (getpropc const 'const nil wrld))
    ((unless (and (quotep qval)
                  (consp (cdr qval))
                  (eq (cddr qval) nil)))
     (raise
      "Internal error: ~
                the CONST property ~x0 of ~x1 is not a quoted constant."
      qval const)))
   (unquote qval))))