REWRITES_CONV : ('a * (term -> 'b)) net -> term -> 'b
- SYNOPSIS
-
Apply a prioritized conversion net to the term at the top level.
- DESCRIPTION
-
The underlying machinery in rewriting and simplification assembles
(conditional) rewrite rules and other conversions into a net, including a
priority number so that, for example, pure rewrites get applied before
conditional rewrites. If net is such a net (for example, constructed using
mk_rewrites and net_of_thm), then REWRITES_CONV net is a conversion that
uses all those conversions at the toplevel to attempt to rewrite the term. If a
conditional rewrite is applied, the resulting theorem will have an assumption.
This is the primitive operation that performs HOL Light rewrite steps.
- FAILURE CONDITIONS
-
Fails when applied to the term if none of the conversions in the net are
applicable.
- SEE ALSO
-
GENERAL_REWRITE_CONV, GEN_REWRITE_CONV, mk_rewrites, net_of_conv, net_of_thm,
REWRITE_CONV.