inductive Duper.LazyList (α : Type u) : Type u

• nil {α : Type u} : LazyList α
• cons {α : Type u} (hd : α) (tl : LazyList α) : LazyList α
• delayed {α : Type u} (t : Thunk (LazyList α)) : LazyList α

def Duper.List.toLazy {α : Type u} : List α → LazyList α

Equations

• Duper.List.toLazy [] = Duper.LazyList.nil
• Duper.List.toLazy (h :: t) = Duper.LazyList.cons h (Duper.List.toLazy t)

instance Duper.LazyList.instInhabited {α : Type u} : Inhabited (LazyList α)

Equations

• Duper.LazyList.instInhabited = { default := Duper.LazyList.nil }

partial def Duper.LazyList.nats (i : Nat) : LazyList Nat

@[irreducible]

def Duper.LazyList.size {α : Type u} : LazyList α → Nat

Equations

• Duper.LazyList.nil.size = 0
• (Duper.LazyList.cons hd tl).size = tl.size + 1
• (Duper.LazyList.delayed t).size = t.get.size + 1

@[inline]

def Duper.LazyList.pure {α : Type u} : α → LazyList α

Equations

• Duper.LazyList.pure x✝ = Duper.LazyList.cons x✝ Duper.LazyList.nil

@[irreducible]

def Duper.LazyList.isEmpty {α : Type u} : LazyList α → Bool

Equations

• Duper.LazyList.nil.isEmpty = true
• (Duper.LazyList.cons hd tl).isEmpty = false
• (Duper.LazyList.delayed t).isEmpty = t.get.isEmpty

@[irreducible]

def Duper.LazyList.toList {α : Type u} : LazyList α → List α

Equations

• Duper.LazyList.nil.toList = []
• (Duper.LazyList.cons hd tl).toList = hd :: tl.toList
• (Duper.LazyList.delayed t).toList = t.get.toList

@[irreducible]

def Duper.LazyList.head {α : Type u} [Inhabited α] : LazyList α → α

Equations

• Duper.LazyList.nil.head = default
• (Duper.LazyList.cons hd tl).head = hd
• (Duper.LazyList.delayed t).head = t.get.head

@[irreducible]

def Duper.LazyList.tail {α : Type u} : LazyList α → LazyList α

Equations

• Duper.LazyList.nil.tail = Duper.LazyList.nil
• (Duper.LazyList.cons hd tl).tail = tl
• (Duper.LazyList.delayed t).tail = t.get.tail

@[irreducible]

def Duper.LazyList.append {α : Type u} : LazyList α → LazyList α → LazyList α

Equations

• Duper.LazyList.nil.append x✝ = x✝
• (Duper.LazyList.cons a as).append x✝ = Duper.LazyList.cons a (Duper.LazyList.delayed { fn := fun (x : Unit) => as.append x✝ })
• (Duper.LazyList.delayed as).append x✝ = as.get.append x✝

instance Duper.LazyList.instAppend {α : Type u} : Append (LazyList α)

Equations

• Duper.LazyList.instAppend = { append := Duper.LazyList.append }

@[irreducible, specialize #[]]

def Duper.LazyList.map {α : Type u} {β : Type v} (f : α → β) : LazyList α → LazyList β

Equations

• Duper.LazyList.map f Duper.LazyList.nil = Duper.LazyList.nil
• Duper.LazyList.map f (Duper.LazyList.cons hd tl) = Duper.LazyList.cons (f hd) (Duper.LazyList.map f tl)
• Duper.LazyList.map f (Duper.LazyList.delayed t) = Duper.LazyList.delayed { fn := fun (x : Unit) => Duper.LazyList.map f t.get }

@[irreducible, specialize #[]]

def Duper.LazyList.map₂ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) : LazyList α → LazyList β → LazyList δ

Equations

• Duper.LazyList.map₂ f Duper.LazyList.nil x✝ = Duper.LazyList.nil
• Duper.LazyList.map₂ f x✝ Duper.LazyList.nil = Duper.LazyList.nil
• Duper.LazyList.map₂ f (Duper.LazyList.cons a as) (Duper.LazyList.cons b bs) = Duper.LazyList.cons (f a b) (Duper.LazyList.delayed { fn := fun (x : Unit) => Duper.LazyList.map₂ f as bs })
• Duper.LazyList.map₂ f (Duper.LazyList.delayed as) x✝ = Duper.LazyList.map₂ f as.get x✝
• Duper.LazyList.map₂ f x✝ (Duper.LazyList.delayed bs) = Duper.LazyList.map₂ f x✝ bs.get

@[irreducible]

def Duper.LazyList.interleave {α : Type u} : LazyList α → LazyList α → LazyList α

Equations

• Duper.LazyList.nil.interleave x✝ = x✝
• (Duper.LazyList.cons a as).interleave x✝ = Duper.LazyList.cons a (Duper.LazyList.delayed { fn := fun (x : Unit) => x✝.interleave as })
• (Duper.LazyList.delayed as).interleave x✝ = Duper.LazyList.delayed { fn := fun (x : Unit) => as.get.interleave x✝ }

def Duper.LazyList.interleaveN {α : Type u} : Array (LazyList α) → LazyList α

Equations

• Duper.LazyList.interleaveN x = Duper.LazyList.interleaveN.iNrec (Std.Queue.enqueueAll x.toList Std.Queue.empty)

partial def Duper.LazyList.interleaveN.iNrec {α : Type u} (q : Std.Queue (LazyList α)) : LazyList α

def Duper.LazyList.interleaveω {α : Type u} : LazyList (LazyList α) → LazyList α

Equations

• x.interleaveω = Duper.LazyList.interleaveω.iωrec 0 0 Std.Queue.empty x

partial def Duper.LazyList.interleaveω.iωrec {α : Type u} (i j : Nat) (q : Std.Queue (LazyList α)) (x : LazyList (LazyList α)) : LazyList α

def Duper.LazyList.bindω {α : Type u} {β : Type v} (xs : LazyList α) (f : α → LazyList β) : LazyList β

Equations

• xs.bindω f = (Duper.LazyList.map f xs).interleaveω

@[inline]

def Duper.LazyList.zip {α : Type u} {β : Type v} : LazyList α → LazyList β → LazyList (α × β)

Equations

• Duper.LazyList.zip = Duper.LazyList.map₂ Prod.mk

@[irreducible]

def Duper.LazyList.join {α : Type u} : LazyList (LazyList α) → LazyList α

Equations

• Duper.LazyList.nil.join = Duper.LazyList.nil
• (Duper.LazyList.cons a as).join = a.append (Duper.LazyList.delayed { fn := fun (x : Unit) => as.join })
• (Duper.LazyList.delayed t).join = t.get.join

@[inline]

def Duper.LazyList.bind {α : Type u} {β : Type v} (x : LazyList α) (f : α → LazyList β) : LazyList β

Equations

• x.bind f = (Duper.LazyList.map f x).join

instance Duper.LazyList.isMonad : Monad LazyList

Equations

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

instance Duper.LazyList.instAlternative : Alternative LazyList

Equations

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

@[irreducible]

def Duper.LazyList.approx {α : Type u} : Nat → LazyList α → List α

Equations

• Duper.LazyList.approx 0 x✝ = []
• Duper.LazyList.approx x✝ Duper.LazyList.nil = []
• Duper.LazyList.approx i.succ (Duper.LazyList.cons a as) = a :: Duper.LazyList.approx i as
• Duper.LazyList.approx i.succ (Duper.LazyList.delayed as) = Duper.LazyList.approx (i + 1) as.get

@[specialize #[]]

partial def Duper.LazyList.iterate {α : Type u} (f : α → α) : α → LazyList α

@[specialize #[]]

partial def Duper.LazyList.iterate₂ {α : Type u} (f : α → α → α) : α → α → LazyList α

@[irreducible, specialize #[]]

def Duper.LazyList.filter {α : Type u} (p : α → Bool) : LazyList α → LazyList α

Equations

• Duper.LazyList.filter p Duper.LazyList.nil = Duper.LazyList.nil
• Duper.LazyList.filter p (Duper.LazyList.cons hd tl) = if p hd = true then Duper.LazyList.cons hd (Duper.LazyList.filter p tl) else Duper.LazyList.filter p tl
• Duper.LazyList.filter p (Duper.LazyList.delayed t) = Duper.LazyList.delayed { fn := fun (x : Unit) => Duper.LazyList.filter p t.get }

partial def Duper.LazyList.cycle {α : Type u} : LazyList α → LazyList α

partial def Duper.LazyList.repeats {α : Type u} : α → LazyList α

@[irreducible]

def Duper.LazyList.inits {α : Type u} : LazyList α → LazyList (LazyList α)

Equations

• One or more equations did not get rendered due to their size.
• Duper.LazyList.nil.inits = Duper.LazyList.cons Duper.LazyList.nil Duper.LazyList.nil
• (Duper.LazyList.delayed t).inits = t.get.inits

def Duper.LazyList.addOpenBracket (s : String) : String

Equations

• Duper.LazyList.addOpenBracket s = if s.isEmpty = true then "[" else s

@[irreducible]

def Duper.LazyList.approxToStringAux {α : Type u} [ToString α] : Nat → LazyList α → String → String

Equations

• Duper.LazyList.approxToStringAux x✝¹ Duper.LazyList.nil x✝ = (if x✝.isEmpty = true then "[" else x✝) ++ "]"
• Duper.LazyList.approxToStringAux 0 x✝¹ x✝ = (if x✝.isEmpty = true then "[" else x✝) ++ ", ..]"
• Duper.LazyList.approxToStringAux n.succ (Duper.LazyList.cons a as) x✝ = Duper.LazyList.approxToStringAux n as ((if x✝.isEmpty = true then "[" else x✝ ++ ", ") ++ toString a)
• Duper.LazyList.approxToStringAux x✝¹ (Duper.LazyList.delayed as) x✝ = Duper.LazyList.approxToStringAux x✝¹ as.get x✝

def Duper.LazyList.approxToString {α : Type u} [ToString α] (as : LazyList α) (n : Nat := 10) : String

Equations

• as.approxToString n = Duper.LazyList.approxToStringAux n as ""

instance Duper.LazyList.instToString {α : Type u} [ToString α] : ToString (LazyList α)

Equations

• Duper.LazyList.instToString = { toString := fun (as : Duper.LazyList α) => as.approxToString }

def List.lazySubsequences {α : Type u} : List α → Duper.LazyList (List α)

Equations

• [].lazySubsequences = Duper.LazyList.cons [] Duper.LazyList.nil
• (h :: t).lazySubsequences = t.lazySubsequences ++ Duper.LazyList.delayed { fn := fun (x : Unit) => Duper.LazyList.map (List.cons h) t.lazySubsequences }