Bhavik Mehta (Mar 08 2021 at 03:27):
Here's my example:
import combinatorics.simple_graph.basic example : true ↔ true := begin symmetry, end
fails with the error
invalid apply tactic, failed to unify true ↔ true with ?m_2.adj ?m_3 ?m_4 ↔ ?m_2.adj ?m_4 ?m_3
and doesn't fail without the import.
Presumably this is from the symm attribute on
simple_graph.edge_symm - should this be removed?
Kyle Miller (Mar 08 2021 at 06:13):
Yes, that attribute should be removed. There are no uses of
symmetry when it comes to
simple_graph.adj, but if it were somehow useful a fix would be to have a lemma that's an implication rather than a bi-implication:
@[symm] lemma edge_symm' (u v : V) : G.adj u v → G.adj v u := λ x, G.sym x
Bhavik Mehta (Mar 17 2021 at 16:11):
Done both in #6736
Last updated: May 14 2021 at 12:18 UTC