Minimal-runes
Compute runes to leave enabled
Example Form:
(minimal-runes (defun proper-cons-nest-p (x)
(declare (xargs :guard (pseudo-termp x)))
(cond ((symbolp x) nil)
((fquotep x) (true-listp (cadr x)))
((eq (ffn-symb x) 'cons)
(proper-cons-nest-p (fargn x 2)))
(t nil)))
:verbose-p :minimal)
General Form:
(minimal-runes event-form
:verbose-p v ; default = :normal ;
:multiplier m ; default = 1 ;
:name n ; default = nil ;
)
where event-form is an embeddable event (see events); v is
nil, :minimal, :normal, or t; m is a positive
rational number; and n is nil or a logical-name. The value returned is
an error-triple (mv erp runes state), where erp is typically
nil and runes is a list of runes that suffice to admit
the indicated event-form; moreover, if the multiplier m is less
than 1, then the event is admitted with fewer prover steps.
This utility is essentially identical to removable-runes —
indeed, they share the same algorithm — except that instead of returning
a list of runes to disable, it returns a list of runes sufficient for
admitting the event. See removable-runes for detailed documentation.
There is one other difference: minimal-runes has an extra keyword
argument, :name. If :name is supplied then its value must be a
symbol, n, that is a logical-name. In that case, the list of
runes returned is modified by first removing all those in (current-theory
n); see current-theory.
