Hi Barton,
> Two defrules can display the same, yet be different:
Yes, this is a shortcoming of the current system.
However it's easy to remedy -- just carry the matchdeclare
info along with the rule definition and display the rule as
r1 : f(x) -> x f(x - 1) assuming mapatom(x)
or something like that.
> Maybe somebody would like to take this on as a project---the
> defrule code is too recondite for me to hack.
Well, I am confident that I understand the rule code
well enough to modify it. But I don't know what "this" you mean.
> As it is, defrule isn't geared toward applying function
> identities that have dummy variables --- defrule is
> more suited for applying substitutions to expressions.
I don't understand what you mean here; defrule observes
matchdeclare predicates (same as tellsimp, tellsimpafter,
and defmatch). At this point you'll have to present some
examples in order to help me understand the problem.
There are bugs in the rule-processing code, and there
are some new features which we might bolt onto it.
Be that as it may, I don't see a need to either replace
it wholesale, or to construct a parallel system which is
similar but different. Maybe you can clarify what is your
larger goal here.
All the best,
Robert