mathlib

mathlib copied to clipboard

finset.fin_range n is just finset.univ, so we inline its definition in the fintype (fin n) instance to avoid people trying to use it.

---

I think list.fin_range should refer to finset.univ in the docstring.

I think we will need to add a new case to tactic.norm_num.eval_finset to handle univ : finset (fin n). Let me know if you're having trouble with that.

There already is a case to handle univ : finset α. Is that not enough?

I don't think so, the case for univ just opens up the fintype instance and goes in recursion on the expression it finds in the fintype.elems field.

Then I have no idea what to do! 😅

I've pushed a commit that should work, but we'll have to wait for all the dependencies of the test to build to find out.

Doesn't seem to have worked 😢

Sorry, this dropped off my radar. Now it works! (for the one test file, on my machine...)

It's quite hard to parse the norm_num diff here.

Could you spin out a PR that just reorders finset/mutliset/list to list/multiset/finset first, since I think that reorder is what's making the diff painful.

Okay: #15840.

@YaelDillies bump on this - it seems sensible enough to me but it needs a merge of master

Thanks for splitting out the reorder, the norm_num diff is now much easier to follow!

:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests