REDUCE_RULE

reduceLib.REDUCE_RULE : thm -> thm

Performs arithmetic or boolean reduction on a theorem at all levels possible.

REDUCE_RULE attempts to transform a theorem by applying REDUCE_CONV.

Failure

Never fails, but may just return the original theorem.

Example

> reduceLib.REDUCE_RULE (ASSUME “x = 100 + (60 - 17)”);
val it = [.] ⊢ x = 143 : thm

> reduceLib.REDUCE_RULE (REFL “100 + 12 DIV 6”);
val it = ⊢ T : thm

See also

reduceLib.RED_CONV, reduceLib.REDUCE_CONV, reduceLib.REDUCE_TAC