		Search-engine friendly clone of the ACL2 documentation.

Context

Change-context

Modifying constructor for context structures.

Syntax

(change-context x 
                [:tops <tops>] 
                [:types <types>] 
                [:functions <functions>] 
                [:variables <variables>] 
                [:obligation-vars <obligation-vars>] 
                [:obligation-hyps <obligation-hyps>])

This is an often useful alternative to make-context.

We construct a new context structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-context

(defmacro change-context (x &rest args)
  (std::change-aggregate
       'context
       x args
       '((:tops . context->tops)
         (:types . context->types)
         (:functions . context->functions)
         (:variables . context->variables)
         (:obligation-vars . context->obligation-vars)
         (:obligation-hyps . context->obligation-hyps))
       'change-context
       'nil))