Commit 2024-09-26 17:43 aaff5ad5
View on Github →chore(Data/Fin/Tuple): generalize Type
to Sort
(#17161)
Generalize definitions and theorems in Data/Fin/Tuple/Basic
to take in Sort
by default instead of Type
.
The exceptions are theorems that interact with existing type classes such as Preorder
, Prod
, and Set
, which expect Type
.
For instance, the following is added specifically for some theorems about Preorder
:
variable {α : Fin (n + 1) → Type*}
-- instead of variable {α : Fin (n + 1) → Sort*}