		Search-engine friendly clone of the ACL2 documentation.

Atc-context

Make-atc-context

Basic constructor macro for atc-context structures.

Syntax

(make-atc-context [:preamble <preamble>] 
                  [:premises <premises>])

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

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

Definition

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

Macro: make-atc-context

(defmacro make-atc-context (&rest args)
  (std::make-aggregate 'atc-context
                       args '((:preamble) (:premises))
                       'make-atc-context
                       nil))

Function: atc-context

(defun atc-context (preamble premises)
  (declare (xargs :guard (and (true-listp preamble)
                              (atc-premise-listp premises))))
  (declare (xargs :guard t))
  (let ((__function__ 'atc-context))
    (declare (ignorable __function__))
    (b* ((preamble (mbe :logic (list-fix preamble)
                        :exec preamble))
         (premises (mbe :logic (atc-premise-list-fix premises)
                        :exec premises)))
      (list (cons 'preamble preamble)
            (cons 'premises premises)))))