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*}

Estimated changes

modified def Fin.append
modified theorem Fin.append_assoc
modified theorem Fin.append_cast_left
modified theorem Fin.append_cast_right
modified theorem Fin.append_comp_rev
modified theorem Fin.append_cons
modified theorem Fin.append_elim0
modified theorem Fin.append_left
modified theorem Fin.append_left_eq_cons
modified theorem Fin.append_left_nil
modified theorem Fin.append_left_snoc
modified theorem Fin.append_rev
modified theorem Fin.append_right
modified theorem Fin.append_right_cons
modified theorem Fin.append_right_eq_snoc
modified theorem Fin.append_right_nil
modified theorem Fin.append_snoc
modified theorem Fin.comp_cons
modified theorem Fin.comp_init
modified theorem Fin.comp_snoc
modified theorem Fin.comp_tail
modified def Fin.consInduction
modified theorem Fin.cons_eq_append
modified theorem Fin.cons_one
modified theorem Fin.cons_snoc_eq_snoc_cons
modified theorem Fin.elim0_append
modified def Fin.extractNth
modified theorem Fin.init_def
modified theorem Fin.insertNth_rev
modified theorem Fin.range_cons
modified theorem Fin.repeat_add
modified theorem Fin.repeat_apply
modified theorem Fin.repeat_comp_rev
modified theorem Fin.repeat_one
modified theorem Fin.repeat_rev
modified theorem Fin.repeat_succ
modified theorem Fin.repeat_zero
modified def Fin.snocInduction
modified theorem Fin.snoc_cast_add
modified theorem Fin.snoc_comp_castSucc
modified theorem Fin.snoc_comp_cast_add
modified theorem Fin.snoc_comp_nat_add
modified theorem Fin.snoc_eq_append
modified theorem Fin.snoc_zero
modified theorem Fin.tail_def
modified theorem Fin.tail_init_eq_init_tail
modified def Fin.«repeat»