		Search-engine friendly clone of the ACL2 documentation.

Svl-aliasdb

Make-svl-aliasdb

Basic constructor macro for svl-aliasdb structures.

Syntax

(make-svl-aliasdb [:this <this>] 
                  [:sub <sub>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-svl-aliasdb

(defmacro make-svl-aliasdb (&rest args)
  (std::make-aggregate 'svl-aliasdb
                       args '((:this) (:sub))
                       'make-svl-aliasdb
                       nil))

Function: svl-aliasdb

(defun svl-aliasdb (this sub)
  (declare (xargs :guard (and (alias-alist-p this)
                              (svl-aliasdb-alist-p sub))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'svl-aliasdb))
    (declare (ignorable acl2::__function__))
    (b* ((this (mbe :logic (alias-alist-fix this)
                    :exec this))
         (sub (mbe :logic (svl-aliasdb-alist-fix sub)
                   :exec sub)))
      (list this sub))))