issue #1535: have `library_search` call `symmetry` before...

Stream: triage

[Random Issue Bot]

Today I chose issue 1535 for discussion!

have library_search call symmetry before giving up
Created by @Scott Morrison (@semorrison) on 2019-10-09
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 1535 for discussion!

have library_search call symmetry before giving up
Created by @Scott Morrison (@semorrison) on 2019-10-09
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

[Rob Lewis]

I think this is implemented already, right?

import tactic.suggest

constants P Q : Prop

axiom pq : P ↔ Q

example : Q ↔ P := by library_search

constants a b : ℕ

axiom ab : a = b

example : b = a := by library_search

[Rob Lewis]

Yes, #2415