Types used in rewrite search. #
inductive tactic.rewrite_search.side :
side represents the side of an equation, either the left or the right.
Convert a side to the string "lhs" or "rhs", for use in tactic name generation.