Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Nov 07 2020 at 14:16):

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?

view this post on Zulip Random Issue Bot (Dec 14 2020 at 14:25):

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?

view this post on Zulip Rob Lewis (Dec 14 2020 at 15:52):

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

view this post on Zulip Rob Lewis (Dec 14 2020 at 15:53):

Yes, #2415


Last updated: May 09 2021 at 15:11 UTC