cache_opt determines which cache to use: NONE means no caching; a standard cache that stores everything is configured by CONSEQ_CONV_default_cache_opt.

The number of steps taken is determined by step_opt. NONE means arbitrarily many; SOME n means at most n. ONCE_DEPTH_CONSEQ_CONV for example uses SOME 1. The parameter redepth determines whether modified terms should be revisited and convL is a basically a list of directed consequence conversions of the conversions that should be applied at subpositions. Its entries consist of a flag, whether to apply the conversion before or after descending into subterms; the weight (i.e. the number of counted steps) for the conversion, and a function from the context (a list of theorems) to the conversion. context provides additional context that might be used.

The first parameter congruence_list is a list of congruence functions that determine how to break down terms. Each element of this list has to be a function congruence context sys dir t which returns a pair of the number of performed steps and a resulting theorem. sys is a callback that allows to apply the depth conversion recursively to subterms. context represents the context that can be used. If you ignore the slightly different return type, the congruence is otherwise a directed consequence conversion. If the congruence can’t be applied, it should either fail or raise an UNCHANGED exception. The callback sys gets the number of already performed steps, a direction and a term. It then returns a accumulated number of steps and a thm option. It never fails. The number of steps is used to abort if the maximum number of globally allowed steps has been reached. The first call of sys should get 0, then the accumulated number has to be passed. The congruence should return the finally accumulated number of steps.