ONCE_DEPTH_CONSEQ_CONV

ConseqConv.ONCE_DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv

Applies a consequence conversion at most once to a sub-terms of a term.

While DEPTH_CONSEQ_CONV c tm applies c repeatedly, ONCE_DEPTH_CONSEQ_CONV c tm applies c at most once.

See also

Conv.DEPTH_CONV, ConseqConv.NUM_DEPTH_CONSEQ_CONV, ConseqConv.DEPTH_CONSEQ_CONV, ConseqConv.DEPTH_STRENGTHEN_CONSEQ_CONV