		Search-engine friendly clone of the ACL2 documentation.

Fconst-dec

Make-fconst-dec

Basic constructor macro for fconst-dec structures.

Syntax

(make-fconst-dec [:core <core>] 
                 [:suffix? <suffix?>])

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

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

Definition

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

Macro: make-fconst-dec

(defmacro make-fconst-dec (&rest args)
  (std::make-aggregate 'fconst-dec
                       args '((:core) (:suffix?))
                       'make-fconst-dec
                       nil))

Function: fconst-dec

(defun fconst-dec (core suffix?)
  (declare (xargs :guard (and (dec-core-fconstp core)
                              (fsuffix-optionp suffix?))))
  (declare (xargs :guard t))
  (let ((__function__ 'fconst-dec))
    (declare (ignorable __function__))
    (b* ((core (mbe :logic (dec-core-fconst-fix core)
                    :exec core))
         (suffix? (mbe :logic (fsuffix-option-fix suffix?)
                       :exec suffix?)))
      (cons :dec (list core suffix?)))))