logic.relation.symm_gen equivalent

Stream: Is there code for X?

[Andrew Carter]

In logic.relation I see a refl_gen and a trans_gen, but is there also an equivalent to a symm_gen hiding somewhere? I realize its trivial, but so is refl_gen so it seems a little bit weird to me that there are just the 2/3 so I'm worried I might be blind.

[Martin Dvořák]

(deleted)

[Mario Carneiro]

surely that exists in the formalization of undirected graphs

[Mario Carneiro]

eh, kind of: src#simple_graph.from_rel

[Mario Carneiro]

it was done ad-hoc with an additional irreflexivity step since that's what was needed. (It is also trivial, so it makes sense that it was not extracted to a lemma.)