		Search-engine friendly clone of the ACL2 documentation.

Amb?-declor/absdeclor-ambig

Make-amb?-declor/absdeclor-ambig

Basic constructor macro for amb?-declor/absdeclor-ambig structures.

Syntax

(make-amb?-declor/absdeclor-ambig [:declor/absdeclor <declor/absdeclor>])

This is the usual way to construct amb?-declor/absdeclor-ambig structures. It simply conses together a structure with the specified fields.

This macro generates a new amb?-declor/absdeclor-ambig structure from scratch. See also change-amb?-declor/absdeclor-ambig, which can "change" an existing structure, instead.

Definition

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

Macro: make-amb?-declor/absdeclor-ambig

(defmacro make-amb?-declor/absdeclor-ambig (&rest args)
  (std::make-aggregate 'amb?-declor/absdeclor-ambig
                       args '((:declor/absdeclor))
                       'make-amb?-declor/absdeclor-ambig
                       nil))

Function: amb?-declor/absdeclor-ambig

(defun amb?-declor/absdeclor-ambig (declor/absdeclor)
  (declare (xargs :guard (amb-declor/absdeclor-p declor/absdeclor)))
  (declare (xargs :guard t))
  (b* ((declor/absdeclor
            (mbe :logic (amb-declor/absdeclor-fix declor/absdeclor)
                 :exec declor/absdeclor)))
    (cons :ambig declor/absdeclor)))