DEPTH_BINOP_CONV : term -> (term -> thm) -> term -> thm
# NUM_REDUCE_CONV `(1 + 2) + (3 * (4 + 5) + 6) + (7 DIV 8)`;; val it : thm = |- (1 + 2) + (3 * (4 + 5) + 6) + 7 DIV 8 = 36
# DEPTH_BINOP_CONV `(+):num->num->num` NUM_REDUCE_CONV `(1 + 2) + (3 * (4 + 5) + 6) + (7 DIV 8)`;; val it : thm = |- (1 + 2) + (3 * (4 + 5) + 6) + 7 DIV 8 = (1 + 2) + (27 + 6) + 0 # NUM_REDUCE_CONV `(1 + 2) + (3 * (4 + 5) + 6) + (7 DIV 8)`;;