@[implicit_reducible]

instance Fin.instUpwardEnumerable {n : Nat} : Std.PRange.UpwardEnumerable (Fin n)

Equations

• Fin.instUpwardEnumerable = { succ? := fun (i : Fin n) => i.addNat? 1, succMany? := fun (m : Nat) (i : Fin n) => i.addNat? m }

@[simp]

theorem Fin.pRangeSucc?_eq {n : Nat} : Std.PRange.succ? = fun (x : Fin n) => x.addNat? 1

@[simp]

theorem Fin.pRangeSuccMany?_eq {n m : Nat} : Std.PRange.succMany? m = fun (x : Fin n) => x.addNat? m

instance Fin.instLawfulUpwardEnumerable {n : Nat} : Std.PRange.LawfulUpwardEnumerable (Fin n)

instance Fin.instLawfulUpwardEnumerableLE {n : Nat} : Std.PRange.LawfulUpwardEnumerableLE (Fin n)

@[implicit_reducible]

instance Fin.instLeast?OfNatNat : Std.PRange.Least? (Fin 0)

Equations

• Fin.instLeast?OfNatNat = { least? := none }

instance Fin.instLawfulUpwardEnumerableLeast?OfNatNat : Std.PRange.LawfulUpwardEnumerableLeast? (Fin 0)

@[simp]

theorem Fin.least?_eq_of_zero : Std.PRange.least? = none

@[implicit_reducible]

instance Fin.instLeast?OfNeZeroNat {n : Nat} [NeZero n] : Std.PRange.Least? (Fin n)

Equations

• Fin.instLeast?OfNeZeroNat = { least? := some 0 }

instance Fin.instLawfulUpwardEnumerableLeast? {n : Nat} [NeZero n] : Std.PRange.LawfulUpwardEnumerableLeast? (Fin n)

@[simp]

theorem Fin.least?_eq {n : Nat} [NeZero n] : Std.PRange.least? = some 0

instance Fin.instLawfulUpwardEnumerableLT {n : Nat} : Std.PRange.LawfulUpwardEnumerableLT (Fin n)

@[implicit_reducible]

instance Fin.instHasSize {n : Nat} : Std.Rxc.HasSize (Fin n)

Equations

• Fin.instHasSize = { size := fun (lo hi : Fin n) => ↑hi + 1 - ↑lo }

theorem Fin.rxcHasSize_eq {n : Nat} : Std.Rxc.HasSize.size = fun (lo hi : Fin n) => ↑hi + 1 - ↑lo

instance Fin.instLawfulHasSize {n : Nat} : Std.Rxc.LawfulHasSize (Fin n)

instance Fin.instIsAlwaysFinite {n : Nat} : Std.Rxc.IsAlwaysFinite (Fin n)

@[implicit_reducible]

instance Fin.instHasSize_1 {n : Nat} : Std.Rxo.HasSize (Fin n)

Equations

• Fin.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance Fin.instLawfulHasSize_1 {n : Nat} : Std.Rxo.LawfulHasSize (Fin n)

instance Fin.instIsAlwaysFinite_1 {n : Nat} : Std.Rxo.IsAlwaysFinite (Fin n)

@[implicit_reducible]

instance Fin.instHasSize_2 {n : Nat} : Std.Rxi.HasSize (Fin n)

Equations

• Fin.instHasSize_2 = { size := fun (lo : Fin n) => n - ↑lo }

theorem Fin.rxiHasSize_eq {n : Nat} : Std.Rxi.HasSize.size = fun (lo : Fin n) => n - ↑lo

instance Fin.instLawfulHasSize_2 {n : Nat} : Std.Rxi.LawfulHasSize (Fin n)

instance Fin.instIsAlwaysFinite_2 {n : Nat} : Std.Rxi.IsAlwaysFinite (Fin n)