		Search-engine friendly clone of the ACL2 documentation.

System

Make-system

Basic constructor macro for system structures.

Syntax

(make-system [:definitions <definitions>] 
             [:constraints <constraints>])

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

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

Definition

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

Macro: make-system

(defmacro make-system (&rest args)
  (std::make-aggregate 'system
                       args '((:definitions) (:constraints))
                       'make-system
                       nil))

Function: system

(defun system (definitions constraints)
  (declare (xargs :guard (and (definition-listp definitions)
                              (constraint-listp constraints))))
  (declare (xargs :guard t))
  (let ((__function__ 'system))
    (declare (ignorable __function__))
    (b* ((definitions (mbe :logic (definition-list-fix definitions)
                           :exec definitions))
         (constraints (mbe :logic (constraint-list-fix constraints)
                           :exec constraints)))
      (cons :system (list (cons 'definitions definitions)
                          (cons 'constraints constraints))))))