Zulip Chat Archive

Stream: general

Topic: library_search on subgroup bot_le


Alex J. Best (Jun 24 2020 at 01:05):

@Scott Morrison (and everyone!) after learning about library_search! I went and looked at some situations where I'd have expected library_search to work but it didn't and still had some issues, here is a MWE: Is there a reason I shouldn't expect library search to work in the second example, despite it doing so in the first?

import tactic
import group_theory.subgroup

example {L : Type} [complete_lattice L] (a : L) : ( : L)  a :=
begin
  library_search, --works (bot_le)
end

example {G : Type} [group G] (a : subgroup G) : ( : subgroup G)  a :=
begin
  library_search!, --fails
end

Scott Morrison (Jun 24 2020 at 03:52):

I'm happy to call that a bug; my model of how library_search! works calls for it being strictly more successful. :-)

Scott Morrison (Jun 24 2020 at 03:52):

Looks like I have some library_search hacking coming up.

Scott Morrison (Jun 24 2020 at 03:53):

I've starred this message, but if you want to file an issue and/or anyone wants to diagnose / solve it themselves, go for it!


Last updated: Dec 20 2023 at 11:08 UTC