Commit 2023-02-28 18:04 4c586d29
View on Github →chore(data/{multiset,finset}/pi): generalize from Type
to Sort
(#18429)
Everything in this file about multiset.pi.cons
generalizes to Sort
.
The parts of the file which don't generalize now use β
instead.
This is motivated by #18417, though I do not know if supporting Sort
is actually important there.
Forward-ported as https://github.com/leanprover-community/mathlib4/pull/2220