Zulip Chat Archive

Stream: Is there code for X?

Topic: (@univ $ perm ι).card = (card ι).factorial


view this post on Zulip Eric Wieser (Dec 03 2020 at 17:29):

Library search isn't finding this anyway - does it exist?

import data.fintype.basic
import data.nat.factorial

example {ι : Type*} [fintype ι] (@finset.univ (equiv.perm ι)).card = (fintype.card ι).factorial := sorry

view this post on Zulip Kevin Buzzard (Dec 03 2020 at 17:32):

Does it exist for ι = fin n?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:34):

Oh, it's docs#fintype.card_equiv docs#fintype.card_perm

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:35):

I guess library_search couldn't unfold perm?

view this post on Zulip Shing Tak Lam (Dec 03 2020 at 17:36):

I think fintype.card_perm needs [decidable_eq \iota]?

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:38):

I think in my real example I already have that, but now lean is rebuilding the universe so I guess I'll never know

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:40):

huh, this is just a library_search quirk - exact fintype.card_perm closed my goal

view this post on Zulip Eric Wieser (Dec 03 2020 at 17:43):

Aha, it's docs#finset.card_univ that I was missing

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:45):

library_search! will unfold more btw

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:45):

Sometiimes that makes the difference.

view this post on Zulip Adam Topaz (Dec 03 2020 at 17:48):

@Rob Lewis Should the tactics docs mention this? (It doesn't look like they do at this point). Where does one make PRs for these docs?

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:50):

Yes, it definitely should. The doc string for docs#tactic.interactive.library_search does actually mention it, but for some reason there's a shorter version being used for the tactic doc entry.

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:51):

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/suggest.lean#L495 is the line that creates the doc entry.

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:51):

In this case, the doc string right above that line is the entry. But we should just delete that and use the doc string on the tactic.

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:51):

I'll do it.

view this post on Zulip Rob Lewis (Dec 03 2020 at 17:56):

#5206


Last updated: May 16 2021 at 05:21 UTC