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)
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
The default setting is