mathlib
mathlib copied to clipboard
refactor(data/finset/fin): Delete `finset.fin_range`
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: