NUM_DEPTH_CONSEQ_CONV : directed_conseq_conv -> int -> directed_conseq_conv
STRUCTURE
ConseqConv
SYNOPSIS
Applies a consequence conversion at most a given number of times to the sub-terms of a term, in bottom-up order.
DESCRIPTION
While
DEPTH_CONSEQ_CONV c tm
applies
c
repeatedly,
NUM_DEPTH_CONSEQ_CONV c n tm
applies it at most n-times.
SEEALSO
DEPTH_CONV
,
ONCE_DEPTH_CONSEQ_CONV
,
DEPTH_CONSEQ_CONV
,
DEPTH_STRENGTHEN_CONSEQ_CONV
HOL
Kananaskis-14