show the generated equivalence relation maintained at the current subterm
Major Section: PROOF-CHECKER-COMMANDS
General Forms: geneqv ; show list of equivalence relations being maintained (geneqv t) ; as above, but pair each relation with a justifying runeThis is an advanced command, whose effect is to print the so-called ``generated equivalence relation'' (or ``geneqv'') that is maintained at the current subterm of the conclusion. That structure is a list of equivalence relations, representing the transitive closure
E of the union of those
relations, such that it suffices to maintain E at the current subterm: if
that subterm, u, is replaced in the goal's conclusion, G, by another
term equivalent to u with respect to E, then the resulting conclusion
is Boolean equivalent to G. Also see defcong.The command `geneqv' prints the above list of equivalence relations, or
more precisely, the list of function symbols for those relations. If however
geneqv is given a non-nil argument, then a list is printed whose
elements are each of the form (s r), where s is the symbol for an
equivalence relation and r is a :congruence rune
justifying the inclusion of s in the list of equivalence relations being
maintained at the current subterm.
