@[simp]

theorem Bool.bnot_eq_bnot (a b : Bool) : (!a) = !b ↔ a = b

@[simp]

theorem Bool.eq_true_iff_eq_true (a b : Bool) : (a = true ↔ b = true) ↔ a = b

@[simp]

theorem Bool.eq_false_iff_eq_false (a b : Bool) : (a = false ↔ b = false) ↔ a = b

theorem Bool.bnot_eq (a b : Bool) : (!a) = b ↔ ¬a = b

theorem Bool.eq_bnot (a b : Bool) : a = !b ↔ ¬a = b

Int

theorem Int.eq_zero_of_lt_neg_iff_lt (i : Int) : (0 < -i ↔ 0 < i) → i = 0

def List.enum' {α : Type u_1} (L : List α) : List (Fin L.length × α)

Equations

• L.enum' = List.enum'.go L L 0 ⋯

def List.enum'.go {α : Type u_1} (L rest : List α) (i : Nat) (h : i + rest.length = L.length) : List (Fin L.length × α)

Equations

• List.enum'.go L [] i x = []
• List.enum'.go L (x :: xs) i h_2 = (⟨i, ⋯⟩, x) :: List.enum'.go L xs (i + 1) ⋯

def Fin.pred? {n : Nat} : Fin n → Option (Fin n)

Equations

• ⟨0, isLt⟩.pred? = none
• ⟨i.succ, h⟩.pred? = some ⟨i, ⋯⟩

def Fin.predCast {n : Nat} : Fin n → Option (Fin n.pred)

if i > 0, then i-1, else none

Equations

• ⟨0, isLt⟩.predCast = none
• ⟨i.succ, h⟩.predCast = some ⟨i, ⋯⟩

def Fin.castPred' {n : Nat} (i : Fin n) : Option (Fin n.pred)

if i < Fin.last n then i, else none

Equations

• i_2.castPred' = i_2.elim0
• i_2.castPred' = if h : ↑i_2 = n_2 then none else some ⟨↑i_2, ⋯⟩

def Fin.succ? {n : Nat} : Fin n → Option (Fin n)

Equations

• i.succ? = i.elim0
• ⟨i, isLt⟩.succ? = if h : i < n then some ⟨i + 1, ⋯⟩ else none

theorem Fin.foldl_induction {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) (P : α → Fin (n + 1) → Prop) (hInit : P init 0) (hSucc : ∀ (a : α) (i : Fin n), P a ⟨↑i, ⋯⟩ → P (f a i) ⟨↑i + 1, ⋯⟩) : P (foldl n f init) ⟨n, ⋯⟩

@[irreducible]

theorem Fin.foldl_induction.loop {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (P : α → Fin (n + 1) → Prop) (hSucc : ∀ (a : α) (i : Fin n), P a ⟨↑i, ⋯⟩ → P (f a i) ⟨↑i + 1, ⋯⟩) (x : α) (i : Fin (n + 1)) (h : P x i) : P (foldl.loop n f x ↑i) ⟨n, ⋯⟩

theorem Fin.foldl_induction' {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) (P : α → Prop) (hInit : P init) (hSucc : ∀ (a : α) (i : Fin n), P a → P (f a i)) : P (foldl n f init)

theorem Fin.foldl_of_comm {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) (i : Fin n) (H : ∀ (acc : α) (i₁ i₂ : Fin n), f (f acc i₁) i₂ = f (f acc i₂) i₁) : ∃ (acc : α), foldl n f init = f acc i

def Function.iterate {α : Sort u_1} (f : α → α) : Nat → α → α

Equations

• Function.iterate f 0 = id
• Function.iterate f n.succ = Function.iterate f n ∘ f

Array

def Array.pop? {α : Type u_1} (A : Array α) : Option (Array α × α)

Equations

• A.pop? = match A.back? with | none => none | some a => some (A.pop, a)

@[simp]

theorem Array.size_pop? {α✝ : Type u_1} {A' : Array α✝} {a : α✝} {A : Array α✝} : A.pop? = some (A', a) → A'.size + 1 = A.size

def Array.maxBy {α : Type u_1} {β : Type u_2} (f : α → β) [Max β] (A : Array α) : Option β

Equations

• Array.maxBy f A = if h : A.size > 0 then let b0 := f A[0]; some (Array.foldl (fun (x1 : β) (x2 : α) => max x1 (f x2)) b0 A 1) else none

theorem Array.mkArray_succ_eq_singleton_append {α : Type u_1} (n : Nat) (a : α) : replicate (n + 1) a = #[a] ++ replicate n a

@[simp]

theorem Array.foldl_cons {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (a : α) (as : List α) : foldl f init { toList := a :: as } = foldl f (f init a) { toList := as }

theorem Array.ofFn_getElem {α : Type u_1} (A : Array α) : (ofFn fun (x : Fin A.size) => A[x]) = A

List

theorem List.Sublist.sizeOf_le {α : Type u_1} [SizeOf α] {L₁ L₂ : List α} : L₁.Sublist L₂ → sizeOf L₁ ≤ sizeOf L₂

def List.distinct {α : Type u_1} [DecidableEq α] (L : List α) : List α

Equations

• L.distinct = List.foldl (fun (x1 : List α) (x2 : α) => List.insert x2 x1) [] L

def List.isDistinct {α : Type u_1} [BEq α] : List α → Bool

Equations

• [].isDistinct = true
• (x_1 :: xs).isDistinct = (!xs.contains x_1 && xs.isDistinct)

def List.fins (n : Nat) : List (Fin n)

Equations

• List.fins n = List.fins.finsAux n n ⋯ []

def List.fins.finsAux (n i : Nat) : i ≤ n → List (Fin n) → List (Fin n)

Equations

• List.fins.finsAux n 0 x_3 x = x
• List.fins.finsAux n i.succ h x = List.fins.finsAux n i ⋯ (⟨i, h⟩ :: x)

@[simp]

theorem List.length_fins (n : Nat) : (fins n).length = n

@[simp]

theorem List.fins_zero : fins 0 = []

theorem List.fins_succ (n : Nat) : fins n.succ = map Fin.castSucc (fins n) ++ [Fin.last n]

@[simp]

theorem List.get_fins {n : Nat} (i : Fin (fins n).length) : (fins n).get i = ⟨↑i, ⋯⟩

@[simp]

theorem List.get_fins' {n i : Nat} (hi : i < n) : (fins n).get ⟨i, ⋯⟩ = ⟨i, hi⟩

@[simp]

theorem List.mem_fins {n : Nat} (x : Fin n) : x ∈ fins n

def TaskIO (α : Type) : Type

Equations

• TaskIO α = IO (Task (Except IO.Error α))

instance TaskIO.instMonad : Monad TaskIO

Equations

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

instance TaskIO.instMonadLiftIO : MonadLift IO TaskIO

Equations

• TaskIO.instMonadLiftIO = { monadLift := fun {α : Type} (io : IO α) => EStateM.map (fun (a : α) => { get := Except.ok a }) io }

def TaskIO.wait {α : Type} (task : TaskIO α) : IO α

Equations

• task.wait = do let task ← task let x ← liftM (IO.wait task) ofExcept x

instance TaskIO.instMonadExceptOfError : MonadExceptOf IO.Error TaskIO

Equations

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

def TaskIO.par {σ : Type u_1} {α : Type u_2} {β : Type} [ForIn IO σ α] (xs : σ) (f : α → TaskIO β) : TaskIO (List β)

Equations

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

def TaskIO.parUnit {σ : Type u_1} {α : Type u_2} [ForIn IO σ α] (xs : σ) (f : α → TaskIO Unit) : TaskIO Unit

Equations

• TaskIO.parUnit xs f = do let _ ← TaskIO.par xs f pure ()

def TaskIO.parTasks {σ : Type u_1} {α : Type u_2} {β : Type} [ForIn IO σ α] (xs : σ) (f : α → IO β) : TaskIO (List β)

Equations

• TaskIO.parTasks xs f = TaskIO.par xs fun (a : α) => liftM (f a).asTask

def TaskIO.parTasksUnit {σ : Type u_1} {α : Type u_2} [ForIn IO σ α] (xs : σ) (f : α → IO Unit) : TaskIO Unit

Equations

• TaskIO.parTasksUnit xs f = TaskIO.parUnit xs fun (a : α) => liftM (f a).asTask

def Option.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : m β

Equations

• none.forIn b f = pure b
• (some a).forIn b f = do let __do_lift ← f a b match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => pure b

instance instForInOption_trestle {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn m (Option α) α

Equations

• instForInOption_trestle = { forIn := fun {β : Type ?u.15} [Monad m] => Option.forIn }

def IO.timeMs {α : Type} (prog : IO α) : IO (Nat × α)

Equations

• prog.timeMs = do let start ← liftM IO.monoMsNow let res ← prog let end_ ← liftM IO.monoMsNow pure (end_ - start, res)

instance instGetElemStringNatCharLtLength_trestle : GetElem String Nat Char fun (s : String) (i : Nat) => i < s.length

Equations

• instGetElemStringNatCharLtLength_trestle = { getElem := fun (x : String) (x_1 : Nat) (x_2 : x_1 < x.length) => match x, x_1, x_2 with | xs, i, x => xs.get { byteIdx := i } }

def randFin (n : Nat) (_h : n > 0) : IO (Fin n)

Equations

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

def IO.randPerm {α : Type} (L : List α) : IO (List α)

Equations

• IO.randPerm L = IO.randPerm.randPermTR L [] 0

def IO.randPerm.randPermTR {α : Type} (L acc : List α) (n : Nat) : IO (List α)

Equations

• IO.randPerm.randPermTR [] acc n = pure acc
• IO.randPerm.randPermTR (x :: xs) acc n = do let idx ← liftM (IO.rand 0 n) let acc' : List α := acc.insertIdx idx x IO.randPerm.randPermTR xs acc' (n + 1)

@[simp]

theorem List.sizeOf_filter {α : Type u_1} [SizeOf α] (f : α → Bool) (L : List α) : sizeOf (filter f L) ≤ sizeOf L

theorem List.sizeOf_filter_lt_of_ne {α : Type u_1} [SizeOf α] (f : α → Bool) (L : List α) (h : filter f L ≠ L) : sizeOf (filter f L) < sizeOf L

def List.subtypeSize {α : Type u_1} [SizeOf α] (L : List α) : List { a : α // sizeOf a < sizeOf L }

Equations

• [].subtypeSize = []
• (x_1 :: xs).subtypeSize = ⟨x_1, ⋯⟩ :: List.map (fun (x : { a : α // sizeOf a < sizeOf xs }) => match x with | ⟨a, h⟩ => ⟨a, ⋯⟩) xs.subtypeSize

unsafe def Array.subtypeSizeUnsafe {α : Type u_1} [SizeOf α] (A : Array α) : Array { a : α // sizeOf a < sizeOf A }

Equations

• A.subtypeSizeUnsafe = unsafeCast A

@[implemented_by Array.subtypeSizeUnsafe]

def Array.subtypeSize {α : Type u_1} [SizeOf α] (A : Array α) : Array { a : α // sizeOf a < sizeOf A }

Equations

• { toList := L }.subtypeSize = { toList := List.map (fun (x : { a : α // sizeOf a < sizeOf L }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) L.subtypeSize }

def List.forPairsM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → α → m PUnit) : List α → m PUnit

Like forDiagM, but only runs f e e' (not f e e).

Equations

• List.forPairsM f [] = pure PUnit.unit
• List.forPairsM f (x_1 :: xs) = do xs.forM (f x_1) List.forPairsM f xs

@[inline]

def Option.expectSome {ε : Type u_1} {α : Type u_2} (err : Unit → ε) : Option α → Except ε α

Equations

• Option.expectSome err none = Except.error (err ())
• Option.expectSome err (some a) = Except.ok a

structure NonemptyList (α : Type u_1) : Type u_1

• hd : α
• tl : List α

@[inline]

def List.expectNonempty {ε : Type u_1} {α : Type u_2} (err : Unit → ε) : List α → Except ε (NonemptyList α)

Equations

• List.expectNonempty err [] = Except.error (err ())
• List.expectNonempty err (x_1 :: xs) = Except.ok { hd := x_1, tl := xs }

def PrinterM (α : Type) : Type

Equations

• PrinterM = StateM String

def PrinterM.putStr : String → PrinterM Unit

Equations

• PrinterM.putStr string state = ((), state.append string)

def PrinterM.run : PrinterM Unit → String

Equations

• x✝.run = (StateT.run x✝ "").snd

instance instMonadPrinterM : Monad PrinterM

Equations

• instMonadPrinterM = inferInstance

@[simp]

theorem Array.ofFn_data {n : Nat} {α : Type u_1} (f : Fin n → α) : (ofFn f).toList = List.map f (List.fins n)