		Search-engine friendly clone of the ACL2 documentation.

Set-ccg-inhibit-output-lst

Control output during CCG termination analysis

Examples:
(set-ccg-inhibit-output-lst '(query))
(set-ccg-inhibit-output-lst '(build/refine size-change))
(set-ccg-inhibit-output-lst *ccg-valid-output-names*) ; inhibit all ccg output
:set-ccg-inhibit-output-lst (build/refine size-change)

General Form:
(set-ccg-inhibit-output-lst lst)

where lst is a form (which may mention state) that evaluates to a list of names, each of which is the name of one of the following ``kinds'' of output produced by the CCG termination analysis.

 query prints the goal, restrictions, and results of each prover 
  query (for a discussion on displaying actual proofs, see 
  set-ccg-display-proofs(yet to be documented).  basics the basic CCG 
  output, enough to follow along, but concise enough to keep from drowning in 
  output performance performance information for the size change analysis 
  build/refine the details of CCG construction and refinement size-change the 
  details of size change analysis counter-example prints out a counter-example 
  that can be useful for debugging failed termination proof attempts.

It is possible to inhibit each kind of output by putting the corresponding name into lst. For example, if 'query is included in (the value of) lst, then no information about individual queries is printed during CCG analysis.

The default setting is '(query performance build/refine size-change). That is, by default only the basic CCG information and counter-example (in the case of a failed proof attempt) are printed. This should hopefully be adequate for most users.