|
|
|---|
|
|
|
|---|
A simple interface for simplifying a term, perhaps under a hypothesis and equivalence context, and with optional guidance from a hint.
This provides a straightforward interface for simplifying a term. It uses the proof checker's pc-rewrite* function. It can handle rewriting under some hypotheses, under a user-provided equivalence relation.
Usage:
(easy-simplify-term (my-fn (foo) (bar baz)) ;; optional keyword args: :hyp (and (integerp baz) (<= 0 baz)) :hint (:in-theory (enable my-fn) :expand ((foo))) :equiv equal :normalize t :rewrite t :repeat 555 :backchain-limit 5)
Important NOTE: The HINT keyword should be given a hint keyword/val list, as in the example above, NOT a list of subgoal or computed hints, e.g. (("Goal" :foo)).