		Search-engine friendly clone of the ACL2 documentation.

Values

Lift-symbol

Lift an ACL2 symbol to a symbol value.

Signature
(lift-symbol sym) → symval
Arguments: sym — Guard (symbolp sym).
Returns: symval — Type (symbol-valuep symval).

This function lifts an ACL2 symbol to the meta level, i.e. to our formalization of ACL2 symbols.

We extract package name and symbol name from the ACL2 symbol, and we build a symbol value that represents that symbol at the meta level.

Definitions and Theorems

Function: lift-symbol

(defun lift-symbol (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((__function__ 'lift-symbol))
    (declare (ignorable __function__))
    (b* ((package (symbol-package-name sym))
         (name (symbol-name sym)))
      (make-symbol-value :package package
                         :name name))))

Theorem: symbol-valuep-of-lift-symbol

(defthm symbol-valuep-of-lift-symbol
  (b* ((symval (lift-symbol sym)))
    (symbol-valuep symval))
  :rule-classes :rewrite)