Find-rules-of-rune
Find the rules named rune
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). Deciphering 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.)
