Zulip Chat Archive

Stream: general

Topic: library_search has been merged


view this post on Zulip Scott Morrison (Mar 29 2019 at 03:36):

library_search is now available on master:

import tactic.interactive

example (a b : ℕ) (h : a ∣ b) (w : b > 0) : a ≤ b :=
by library_search -- says: `exact nat.le_of_dvd w h`

example {a b c : ℕ} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b :=
by library_search -- says `exact (nat.dvd_add_left h₁).mp h₂`

view this post on Zulip Scott Morrison (Mar 29 2019 at 03:37):

Please try it out, and report any unexpected failures. It "should" work on any goal which can be closed by applying exactly one lemma from the currently imported library, then some sequence of applying local hypotheses.

view this post on Zulip Johan Commelin (Mar 29 2019 at 07:20):

Hooray! This is awesome!

view this post on Zulip Patrick Massot (Apr 03 2019 at 19:59):

I just used library_search for the first time. I feel so much smarter than one minute ago...

view this post on Zulip Patrick Massot (Apr 03 2019 at 19:59):

The goal was 1 ∈ ker φ

view this post on Zulip Patrick Massot (Apr 03 2019 at 20:09):

I did it again. I think I'm only a couple of uses away from being addicted.

view this post on Zulip Kevin Buzzard (Apr 03 2019 at 20:20):

I know this is kind of funny, but library_search is a big deal for people like me who don't seem to be able to instantly name every lemma in mathlib.


Last updated: May 12 2021 at 23:13 UTC