FIND-RULES-OF-RUNE

Major Section:  MISCELLANEOUS

General Form:
(find-rules-of-rune rune wrld)

This function finds all the rules in wrld with :rune rune. It returns a list of rules in their internal form (generally as described by the corresponding defrec). Decyphering these rules is difficult since one cannot always look at a rule object and decide what kind of record it is without exploiting many system invariants (e.g., that :rewrite runes only name rewrite-rules).

At the moment this function returns nil if the rune in question is a :refinement rune, because there is no object representing :refinement rules. (:refinement rules cause changes in the 'coarsenings properties.) In addition, if the rune is an :equivalence rune, then congruence rules with that rune will be returned -- because :equivalence lemmas generate some congruence rules -- but the fact that a certain function is now known to be an equivalence relation is not represented by any rule object and so no such rule is returned. (The fact that the function is an equivalence relation is encoded entirely in its presence as a 'coarsening of equal.)