		Search-engine friendly clone of the ACL2 documentation.

Modscope-top

Make-modscope-top

Basic constructor macro for modscope-top structures.

Syntax

(make-modscope-top [:modidx <modidx>])

This is the usual way to construct modscope-top structures. It simply conses together a structure with the specified fields.

This macro generates a new modscope-top structure from scratch. See also change-modscope-top, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-modscope-top

(defmacro make-modscope-top (&rest args)
  (std::make-aggregate 'modscope-top
                       args '((:modidx))
                       'make-modscope-top
                       nil))

Function: modscope-top

(defun modscope-top (modidx)
  (declare (xargs :guard (natp modidx)))
  (declare (xargs :guard t))
  (let ((__function__ 'modscope-top))
    (declare (ignorable __function__))
    (b* ((modidx (mbe :logic (nfix modidx)
                      :exec modidx)))
      (cons :top modidx))))