		Search-engine friendly clone of the ACL2 documentation.

Atc-generation-contexts

Atc-context-extend

Extend a context with a list of premises.

Signature
(atc-context-extend context premises) → new-context
Arguments: context — Guard (atc-contextp context).; premises — Guard (atc-premise-listp premises).
Returns: new-context — Type (atc-contextp new-context).

Definitions and Theorems

Function: atc-context-extend

(defun atc-context-extend (context premises)
  (declare (xargs :guard (and (atc-contextp context)
                              (atc-premise-listp premises))))
  (let ((__function__ 'atc-context-extend))
    (declare (ignorable __function__))
    (change-atc-context
         context
         :premises (append (atc-context->premises context)
                           premises))))

Theorem: atc-contextp-of-atc-context-extend

(defthm atc-contextp-of-atc-context-extend
  (b* ((new-context (atc-context-extend context premises)))
    (atc-contextp new-context))
  :rule-classes :rewrite)