		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-context

A context for warnings.

Contexts are usually vl-context1s. However, for more generality, you can use any arbitrary object as a context. The proper way to do this is to wrap it using (vl-context x).

Macro: vl-context

(defmacro vl-context (x)
  (cons 'vl-context-fix (cons x 'nil)))

Macro: make-vl-context

(defmacro make-vl-context (&rest args)
  (cons 'vl-context
        (cons (cons 'make-vl-context1 args)
              'nil)))

Subtopics

Vl-pp-ctxelement-summary: Print a short, human-friendly description of a vl-ctxelement-p.
Ctxexprs: Functions for gathering expressions and the context in which they occur.
Vl-pp-ctxelement-full: Pretty-print a full vl-ctxelement-p.
Vl-context-fix
Vl-ctxelement-summary: Get a short, human-friendly string describing a vl-ctxelement-p.
Vl-context-summary: Get a short, human-friendly string describing a vl-context-p.
Vl-context-p
Vl-pp-context-summary: Print a short, human-friendly string describing a vl-context-p.
Vl-pp-context-full: Pretty-print a full vl-context-p.