def Vect.from_list {A : Type u_1} {n : Nat} (ℓ : List A) : ℓ.length = n → Vect n A

Equations

• ↑[] x_3 = []
• ↑(x_3 :: tl) h = x_3 :: ↑tl ⋯

def Vect.to_list {n : Nat} {A : Type u_1} : Vect n A → List A

Equations

• Vect.to_list = Vect.fold [] List.cons

instance instCoeOutVectList {n : Nat} {T : Type u_1} : CoeOut (Vect n T) (List T)

Equations

• instCoeOutVectList = { coe := Vect.to_list }

instance instCoeDepListNilVectOfNatNat {A : Type u_1} : CoeDep (List A) [] (Vect 0 A)

Equations

• instCoeDepListNilVectOfNatNat = { coe := [] }

instance instCoeDepListConsNilVectOfNatNat {A : Type u_1} {t1 : A} : CoeDep (List A) [t1] (Vect 1 A)

Equations

• instCoeDepListConsNilVectOfNatNat = { coe := ↑[t1] ⋯ }

instance instCoeDepListConsNilVectOfNatNat_1 {A : Type u_1} {t1 t2 : A} : CoeDep (List A) [t1, t2] (Vect 2 A)

Equations

• instCoeDepListConsNilVectOfNatNat_1 = { coe := ↑[t1, t2] ⋯ }

instance instCoeDepListConsNilVectOfNatNat_2 {A : Type u_1} {t1 t2 t3 : A} : CoeDep (List A) [t1, t2, t3] (Vect 3 A)

Equations

• instCoeDepListConsNilVectOfNatNat_2 = { coe := ↑[t1, t2, t3] ⋯ }

instance instCoeDepListConsNilVectOfNatNat_3 {A : Type u_1} {t1 t2 t3 t4 : A} : CoeDep (List A) [t1, t2, t3, t4] (Vect 4 A)

Equations

• instCoeDepListConsNilVectOfNatNat_3 = { coe := ↑[t1, t2, t3, t4] ⋯ }

instance instCoeDepListConsNilVectOfNatNat_4 {A : Type u_1} {t1 t2 t3 t4 t5 : A} : CoeDep (List A) [t1, t2, t3, t4, t5] (Vect 5 A)

Equations

• instCoeDepListConsNilVectOfNatNat_4 = { coe := ↑[t1, t2, t3, t4, t5] ⋯ }

instance instCoeDepListConsNilVectOfNatNat_5 {A : Type u_1} {t1 t2 t3 t4 t5 t6 : A} : CoeDep (List A) [t1, t2, t3, t4, t5, t6] (Vect 6 A)

Equations

• instCoeDepListConsNilVectOfNatNat_5 = { coe := ↑[t1, t2, t3, t4, t5, t6] ⋯ }

def Vect.unexpand_nil : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Vect.unexpand_cons : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.