inductive myProd1 : Type

• building_a_pair : ℤ → ℤ → myProd1

inductive myProd1' : Type

• building_a_pair (a : ℤ) (b : ℕ) : myProd1'

inductive myProd1'' : Type

• building_a_pair (b : ℕ) (a : ℤ) : myProd1''

inductive myProd2 (α : Type) : Type

• building_a_pair {α : Type} (a : α) : ℤ → myProd2 α

inductive myProd3 (α : Type u_1) : Type u_1

• building_a_pair {α : Type u_1} (a : α) : ℤ → myProd3 α

def first_coord (p : myProd3 String) : String

Equations

• first_coord (myProd3.building_a_pair a a_1) = a

structure studentDetails : Type

• firstName : String
• midlleName : String
• lastName : String
• UID : ℤ

structure myFiniteSet : Type

• n : ℤ
• val : ℤ
• isLT : self.val < self.n

inductive myList (n : ℕ) : Type

• empty {n : ℕ} : myList n
• build {n : ℕ} (L : myList n) (i : ℕ) (a : i < n) : myList n

def tail_of_myList {n : ℕ} (L : myList n) : Option ℕ

Equations

• tail_of_myList myList.empty = none
• tail_of_myList (L_2.build i a) = some i

def a₀ : myList 4

Equations

• a₀ = myList.empty

def a₁ : myList 4

Equations

• a₁ = a₀.build 1 a₁._proof_1

def a₁₂ : myList 4

Equations

• a₁₂ = a₁.build 2 a₁₂._proof_2

def a₁₃ : myList 4

Equations

• a₁₃ = a₁.build 3 a₁₃._proof_3

def a₁₁ : myList 4

Equations

• a₁₁ = a₁.build 1 a₁._proof_1

def a₂ : myList 4

Equations

• a₂ = a₀.build 2 a₁₂._proof_2

def a₃ : myList 4

Equations

• a₃ = a₀.build 3 a₁₃._proof_3

inductive ValidList (n : ℕ) : Option ℕ → Type

• nil {n : ℕ} : ValidList n none
• cons {n : ℕ} (k : ℕ) (hk : 1 ≤ k ∧ k ≤ n) {last : Option ℕ} (tail : ValidList n last) (h_ne : k ≠ last.getD 0) : ValidList n (some k)

def b₁ : ValidList 5 (some 1)

Equations

• b₁ = ValidList.cons 1 b₁._proof_4 ValidList.nil b₁._proof_5

def b₁₂ : ValidList 5 (some 2)

Equations

• b₁₂ = ValidList.cons 2 b₁₂._proof_6 b₁ b₁₂._proof_8

def tail {a : Option ℕ} {n : ℕ} (L : ValidList n a) : Option ℕ

Equations

• tail ValidList.nil = none
• _root_.tail (ValidList.cons k hk tail h_ne) = some k

def ValidList.length {n : ℕ} {last : Option ℕ} (l : ValidList n last) : ℕ

Equations

• ValidList.nil.length = 0
• (ValidList.cons k hk tail h_ne).length = 1 + tail.length

def mat1 : Matrix (Fin 2) (Fin 2) ℤ

Equations

• mat1 m n = match (↑m, ↑n) with | (0, 1) => 1 | (1, 0) => -1 | x => 0

def tree_to_mylist (M : Matrix (Fin 2) (Fin 2) ℤ) (L : myList 4) : List (Matrix (Fin 2) (Fin 2) ℤ)

Equations

• tree_to_mylist M myList.empty = [M]
• tree_to_mylist M (star.build k a) = ↑k * M :: tree_to_mylist M star

def a₂₄ : List (Fin 17)

Equations

• a₂₄ = [⟨2, a₂₄._proof_9⟩, ⟨4, a₂₄._proof_10⟩]

def list_to_mat (M : Matrix (Fin 2) (Fin 2) ℤ) (L : List (Fin 17)) : List (Matrix (Fin 2) (Fin 2) ℤ)

Equations

• list_to_mat M [] = [M]
• list_to_mat M (x :: xs) = ↑↑x * M :: list_to_mat M xs