		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscope

Vl-empty-lexscope

Create a new, empty lexical scope.

Signature
(vl-empty-lexscope) → scope
Returns: scope — Type (vl-lexscope-p scope).

Definitions and Theorems

Function: vl-empty-lexscope$inline

(defun vl-empty-lexscope$inline nil
  (declare (xargs :guard t))
  (let ((__function__ 'vl-empty-lexscope))
    (declare (ignorable __function__))
    (make-vl-lexscope)))

Theorem: vl-lexscope-p-of-vl-empty-lexscope

(defthm vl-lexscope-p-of-vl-empty-lexscope
  (b* ((scope (vl-empty-lexscope$inline)))
    (vl-lexscope-p scope))
  :rule-classes :rewrite)