		Search-engine friendly clone of the ACL2 documentation.

Speed-up-event

Suggest ways to speed up an event.

General Form:

(speed-up-event event
                &key
                :synonym-alist    ; default nil
                :min-time-savings ; default :auto
                :min-event-time   ; default :auto
                :print            ; default :brief
                )

Inputs:

event — (required)

The entire event to speed up (e.g., a defthm form).

:synonym-alist — default nil

A symbol-symbol-alist mapping from synonyms to known event types (e.g., you can declare foo to be treated like defthm by the speed-up tool).

:min-time-savings — default :auto

The minimum time savings to report for a given event (in seconds). Time savings smaller than this will normally not be printed. If :auto, use the value of the constant *minimum-time-savings-to-report*.

:min-event-time — default :auto

The minimum time for events we should try to speed up (in seconds). Events that take less time will not have speeding up attempted for them. If :auto, use the value of the constant *minimum-event-time-to-speed-up*

:print — default :brief

How much to print (should satisfy print-levelp).

Description:

Wrapping an event in a call of speed-up-event causes attempts to be made to speed it up (e.g., by deleting hints). Currently, only defthm and defrule events are supported.