def readG6Header (s : String) : UInt32

Equations

• readG6Header s = match s.toList with | [] => 0 | h :: tail => h.val - UInt32.ofNatLT 63 readG6Header._proof_1

def addIdx {α : Type} : List α → ℕ → ℕ → List (α × ℕ × ℕ)

Equations

• addIdx [] x✝¹ x✝ = []
• addIdx (h :: t) x✝¹ x✝ = if x✝¹ = x✝ then (h, 0, x✝ + 1) :: addIdx t 1 (x✝ + 1) else (h, x✝¹, x✝) :: addIdx t (x✝¹ + 1) x✝

theorem addIdxLt {α : Type} (l : List α) (n m : ℕ) : n ≤ m → ∀ {x : α} {i j : ℕ}, (x, i, j) ∈ addIdx l n m → i < j

def collectInFinset {α : Type} [DecidableEq α] : List (Bool × α) → Finset α

Equations

• collectInFinset [] = Finset.empty
• collectInFinset ((true, h) :: t) = insert h (collectInFinset t)
• collectInFinset ((false, snd) :: t) = collectInFinset t

theorem collectInFinsetMem {α : Type} [DecidableEq α] (x : α) (l : List (Bool × α)) : x ∈ collectInFinset l ↔ (true, x) ∈ l

def readG6AdjAux (l : List Char) : Finset (Sym2 ℕ)

Equations

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

def readG6Adj (s : String) : Finset (Sym2 ℕ)

Equations

• readG6Adj s = match s.toList with | [] => Finset.empty | head :: t => readG6AdjAux t

def readG6 (s : String) : SimpleGraph (Fin (readG6Header s).toNat)

Equations

• readG6 s = { Adj := fun (u v : Fin (readG6Header s).toNat) => s(↑u, ↑v) ∈ readG6Adj s, symm := ⋯, loopless := ⋯ }

instance instDecidableRelFinToNatReadG6HeaderAdjReadG6 (s : String) : DecidableRel (readG6 s).Adj

Equations

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

def tacticG6_ : Lean.ParserDescr

Equations

• tacticG6_ = Lean.ParserDescr.node `tacticG6_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "g6" false) (Lean.ParserDescr.parser `Lean.Parser.strLit))