def uncurry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) (pair : α × β) : γ

Equations

• uncurry f pair = f pair.1 pair.2

def pairBind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {γ : Type u_1} [Monad m] (f : α → β → m γ) (pair : m α × m β) : m γ

Equations

• pairBind f pair = do let fst ← pair.1 let snd ← pair.2 f fst snd

def tripleBind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {γ : Type u_1} {δ : Type u_1} [Monad m] (f : α → β → γ → m δ) (triple : m α × m β × m γ) : m δ

Equations

• tripleBind f triple = do let __do_lift ← triple.1 let __do_lift_1 ← triple.2.1 let __do_lift_2 ← triple.2.2 f __do_lift __do_lift_1 __do_lift_2

def pairMapM {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {γ : Type u_1} [Monad m] (f : α → β → γ) (pair : m α × m β) : m γ

Equations

• pairMapM f pair = do let fst ← pair.1 let snd ← pair.2 pure (f fst snd)

def tripleMapM {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {γ : Type u_1} {δ : Type u_1} [Monad m] (f : α → β → γ → δ) (triple : m α × m β × m γ) : m δ

Equations

• tripleMapM f triple = do let __do_lift ← triple.1 let __do_lift_1 ← triple.2.1 let __do_lift_2 ← triple.2.2 pure (f __do_lift __do_lift_1 __do_lift_2)

def Fin.coeLt {n : ℕ} {m : ℕ} : n ≤ m → Fin n → Fin m

Equations

• Fin.coeLt h ⟨i_2, h'⟩ = ⟨i_2, ⋯⟩

inductive LengthIndexedList (α : Type u) : ℕ → Type u

• nil: {α : Type u} → LengthIndexedList α 0
• cons: {α : Type u} → {n : ℕ} → α → LengthIndexedList α n → LengthIndexedList α (n + 1)

instance instReprLengthIndexedList : {α : Type u_1} → {a : ℕ} → [inst : Repr α] → Repr (LengthIndexedList α a)

Equations

• instReprLengthIndexedList = { reprPrec := reprLengthIndexedList✝ }

instance instDecidableEqLengthIndexedList : {α : Type u_1} → {a : ℕ} → [inst : DecidableEq α] → DecidableEq (LengthIndexedList α a)

Equations

• instDecidableEqLengthIndexedList = decEqLengthIndexedList✝

def LengthIndexedList.fromList {α : Type u} (l : List α) : LengthIndexedList α l.length

Equations

• LengthIndexedList.fromList [] = LengthIndexedList.nil
• LengthIndexedList.fromList (x :: xs) = LengthIndexedList.cons x (LengthIndexedList.fromList xs)

def LengthIndexedList.map {α : Type u} {β : Type u} (f : α → β) {n : ℕ} : LengthIndexedList α n → LengthIndexedList β n

Equations

• LengthIndexedList.map f LengthIndexedList.nil = LengthIndexedList.nil
• LengthIndexedList.map f (LengthIndexedList.cons a_2 a_3) = LengthIndexedList.cons (f a_2) (LengthIndexedList.map f a_3)

def LengthIndexedList.foldl {α : Type u} {β : Type u} {n : ℕ} (f : β → α → β) (acc : β) : LengthIndexedList α n → β

Equations

• LengthIndexedList.foldl f acc LengthIndexedList.nil = acc
• LengthIndexedList.foldl f acc (LengthIndexedList.cons a_2 a_3) = LengthIndexedList.foldl f (f acc a_2) a_3

def LengthIndexedList.zipWith {α : Type u} {β : Type u} {γ : Type u} {n : ℕ} (f : α → β → γ) : LengthIndexedList α n → LengthIndexedList β n → LengthIndexedList γ n

Equations

• LengthIndexedList.zipWith f LengthIndexedList.nil LengthIndexedList.nil = LengthIndexedList.nil
• LengthIndexedList.zipWith f (LengthIndexedList.cons x_2 xs) (LengthIndexedList.cons y ys) = LengthIndexedList.cons (f x_2 y) (LengthIndexedList.zipWith f xs ys)

def LengthIndexedList.nth {α : Type u} {n : ℕ} (l : LengthIndexedList α n) (i : Fin n) : α

Equations

• (LengthIndexedList.cons x a).nth ⟨0, isLt⟩ = x
• (LengthIndexedList.cons a xs).nth ⟨i_2.succ, h⟩ = xs.nth ⟨i_2, ⋯⟩

instance LengthIndexedList.instGetElemNatLt {α : Type u_1} {n : ℕ} : GetElem (LengthIndexedList α n) ℕ α fun (_xs : LengthIndexedList α n) (i : ℕ) => i < n

Equations

• LengthIndexedList.instGetElemNatLt = { getElem := fun (xs : LengthIndexedList α n) (i : ℕ) (h : i < n) => xs.nth ⟨i, h⟩ }

def LengthIndexedList.NatEq {α : Type u} {n : ℕ} {m : ℕ} : n = m → LengthIndexedList α n → LengthIndexedList α m

Equations

• LengthIndexedList.NatEq ⋯ l = l

def LengthIndexedList.finRange (n : ℕ) : LengthIndexedList (Fin n) n

Equations

• LengthIndexedList.finRange 0 = LengthIndexedList.nil
• LengthIndexedList.finRange m.succ = LengthIndexedList.cons ⟨m, ⋯⟩ (LengthIndexedList.map (Fin.coeLt ⋯) (LengthIndexedList.finRange m))

def tacticPrint_goal_as_error : Lean.ParserDescr

Equations

• tacticPrint_goal_as_error = Lean.ParserDescr.node `tacticPrint_goal_as_error 1024 (Lean.ParserDescr.nonReservedSymbol "print_goal_as_error " false)

def Vector.ofList {α : Type u} (l : List α) : Mathlib.Vector α l.length

Equations

• Vector.ofList l = ⟨l, ⋯⟩

def Vector.ofArray {α : Type u} (a : Array α) : Mathlib.Vector α a.size

Equations

• Vector.ofArray a = Vector.ofList a.toList

instance instParseableTypeVector_sSA {τ : Type u_1} [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (Mathlib.Vector τ n)

Equations

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

def productsList {α : Type u_1} : List (List α) → List (List α)

productsList [xs, ys] = [(x, y) for x in xs for y in ys], extended to arbitary number of arrays.

Equations

• One or more equations did not get rendered due to their size.
• productsList [] = [[]]

def productsArr {α : Type u_1} : Array (Array α) → Array (Array α)

Builds the cartesian product of all arrays in the input. Pretty inefficient right now, as it converts back and forth to lists...

Equations

• productsArr arr = (List.map List.toArray (productsList ((List.map Array.toList ∘ Array.toList) arr))).toArray