LazyList Nondeterminism Monad

inductive 
LazyList: Type u → Type u
LazyList (
α: Type u
α : 
Type u: Type (u + 1)
Type u) where
  | 
nil: {α : Type u} → LazyList α
nil                               : 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
cons: {α : Type u} → α → LazyList α → LazyList α
cons (
hd: α
hd : 
α: Type u
α) (
tl: LazyList α
tl : 
LazyList: Type u → Type u
LazyList 
α: Type u
α)   : 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
t: Thunk (LazyList α)
t : 
Thunk: Type u → Type u
Thunk $ 
LazyList: Type u → Type u
LazyList 
α: Type u
α)  : 
LazyList: Type u → Type u
LazyList 
α: Type u
α

def 
List.toLazy: {α : Type u} → List α → LazyList α
List.toLazy {
α: Type u
α : 
Type u: Type (u + 1)
Type u} : 
List: Type u → Type u
List 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | []     => 
LazyList.nil: {α : Type u} → LazyList α
LazyList.nil
  | 
h: α
h::
t: List α
t   => 
LazyList.cons: {α : Type u} → α → LazyList α → LazyList α
LazyList.cons 
h: α
h (
toLazy: {α : Type u} → List α → LazyList α
toLazy 
t: List α
t)

namespace LazyList
variable {
α: Type u
α : 
Type u: Type (u + 1)
Type u} {
β: Type v
β : 
Type v: Type (v + 1)
Type v} {
δ: Type w
δ : 
Type w: Type (w + 1)
Type w}

instance: {α : Type u} → Inhabited (LazyList α)
instance : 
Inhabited: Type u → Type u
Inhabited (
LazyList: Type u → Type u
LazyList 
α: Type u
α) :=
  ⟨
nil: {α : Type u} → LazyList α
nil⟩

@[inline] def 
pure: α → LazyList α
pure : 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
a: α
a => 
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
a: α
a 
nil: {α : Type u} → LazyList α
nil

partial def 
isEmpty: LazyList α → Bool
isEmpty : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
Bool: Type
Bool
  | 
nil: {α : Type ?u.1027} → LazyList α
nil          => 
true: Bool
true
  | 
cons: {α : Type ?u.1036} → α → LazyList α → LazyList α
cons _ _     => 
false: Bool
false
  | 
delayed: {α : Type ?u.1058} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
isEmpty: LazyList α → Bool
isEmpty 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get

partial def 
toList: LazyList α → List α
toList : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
List: Type u → Type u
List 
α: Type u
α
  | 
nil: {α : Type ?u.1187} → LazyList α
nil          => 
[]: List α
[]
  | 
cons: {α : Type ?u.1199} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as    => 
a: α
a :: 
toList: LazyList α → List α
toList 
as: LazyList α
as
  | 
delayed: {α : Type ?u.1221} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
toList: LazyList α → List α
toList 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get

partial def 
head: {α : Type u} → [inst : Inhabited α] → LazyList α → α
head [
Inhabited: Type u → Type u
Inhabited 
α: Type u
α] : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
α: Type u
α
  | 
nil: {α : Type ?u.1357} → LazyList α
nil          => 
default: {α : Type u} → [self : Inhabited α] → α
default
  | 
cons: {α : Type ?u.1373} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as
Warning: unused variable `as`    => 
a: α
a
  | 
delayed: {α : Type ?u.1393} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
head: [inst : Inhabited α] → LazyList α → α
head 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get

partial def 
tail: {α : Type u} → LazyList α → LazyList α
tail : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
nil: {α : Type ?u.1530} → LazyList α
nil          => 
nil: {α : Type u} → LazyList α
nil
  | 
cons: {α : Type ?u.1541} → α → LazyList α → LazyList α
cons 
a: α
a
Warning: unused variable `a` 
as: LazyList α
as    => 
as: LazyList α
as
  | 
delayed: {α : Type ?u.1561} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
tail: LazyList α → LazyList α
tail 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get

partial def 
append: {α : Type u} → LazyList α → (Unit → LazyList α) → LazyList α
append : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → (
Unit: Type
Unit → 
LazyList: Type u → Type u
LazyList 
α: Type u
α) → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
nil: {α : Type ?u.1704} → LazyList α
nil,          
bs: Unit → LazyList α
bs => 
bs: Unit → LazyList α
bs 
(): Unit
()
  | 
cons: {α : Type ?u.1723} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as,    
bs: Unit → LazyList α
bs => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
a: α
a (
append: LazyList α → (Unit → LazyList α) → LazyList α
append 
as: LazyList α
as 
bs: Unit → LazyList α
bs))
  | 
delayed: {α : Type ?u.1783} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as,   
bs: Unit → LazyList α
bs => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
append: LazyList α → (Unit → LazyList α) → LazyList α
append 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get 
bs: Unit → LazyList α
bs)

instance: {α : Type u} → Append (LazyList α)
instance : 
Append: Type u → Type u
Append (
LazyList: Type u → Type u
LazyList 
α: Type u
α) where
  append 
a: LazyList α
a 
b: LazyList α
b := 
LazyList.append: {α : Type u} → LazyList α → (Unit → LazyList α) → LazyList α
LazyList.append 
a: LazyList α
a (fun _ => 
b: LazyList α
b)

partial def 
interleave: LazyList α → LazyList α → LazyList α
interleave : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
nil: {α : Type ?u.2013} → LazyList α
nil,          
bs: LazyList α
bs  => 
bs: LazyList α
bs
  | 
cons: {α : Type ?u.2031} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as,    
bs: LazyList α
bs  => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
a: α
a (
interleave: LazyList α → LazyList α → LazyList α
interleave 
bs: LazyList α
bs 
as: LazyList α
as))
  | 
delayed: {α : Type ?u.2089} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as,   
bs: LazyList α
bs  => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
interleave: LazyList α → LazyList α → LazyList α
interleave 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get 
bs: LazyList α
bs)

partial def 
map: (α → β) → LazyList α → LazyList β
map (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type v → Type v
LazyList 
β: Type v
β
  | 
nil: {α : Type ?u.2270} → LazyList α
nil          => 
nil: {α : Type v} → LazyList α
nil
  | 
cons: {α : Type ?u.2282} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as    => 
delayed: {α : Type v} → Thunk (LazyList α) → LazyList α
delayed (
cons: {α : Type v} → α → LazyList α → LazyList α
cons (
f: α → β
f 
a: α
a) (
map: (α → β) → LazyList α → LazyList β
map 
f: α → β
f 
as: LazyList α
as))
  | 
delayed: {α : Type ?u.2332} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
delayed: {α : Type v} → Thunk (LazyList α) → LazyList α
delayed (
map: (α → β) → LazyList α → LazyList β
map 
f: α → β
f 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get)

partial def 
map₂: (α → β → δ) → LazyList α → LazyList β → LazyList δ
map₂ (
f: α → β → δ
f : 
α: Type u
α → 
β: Type v
β → 
δ: Type w
δ) : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type v → Type v
LazyList 
β: Type v
β → 
LazyList: Type w → Type w
LazyList 
δ: Type w
δ
  | 
nil: {α : Type ?u.2498} → LazyList α
nil,          _            => 
nil: {α : Type w} → LazyList α
nil
  | _,            
nil: {α : Type ?u.2518} → LazyList α
nil          => 
nil: {α : Type w} → LazyList α
nil
  | 
cons: {α : Type ?u.2536} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as,    
cons: {α : Type ?u.2540} → α → LazyList α → LazyList α
cons 
b: β
b 
bs: LazyList β
bs    => 
delayed: {α : Type w} → Thunk (LazyList α) → LazyList α
delayed (
cons: {α : Type w} → α → LazyList α → LazyList α
cons (
f: α → β → δ
f 
a: α
a 
b: β
b) (
map₂: (α → β → δ) → LazyList α → LazyList β → LazyList δ
map₂ 
f: α → β → δ
f 
as: LazyList α
as 
bs: LazyList β
bs))
  | 
delayed: {α : Type ?u.2607} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as,   
bs: LazyList β
bs           => 
delayed: {α : Type w} → Thunk (LazyList α) → LazyList α
delayed (
map₂: (α → β → δ) → LazyList α → LazyList β → LazyList δ
map₂ 
f: α → β → δ
f 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get 
bs: LazyList β
bs)
  | 
as: LazyList α
as,           
delayed: {α : Type ?u.2644} → Thunk (LazyList α) → LazyList α
delayed 
bs: Thunk (LazyList β)
bs   => 
delayed: {α : Type w} → Thunk (LazyList α) → LazyList α
delayed (
map₂: (α → β → δ) → LazyList α → LazyList β → LazyList δ
map₂ 
f: α → β → δ
f 
as: LazyList α
as 
bs: Thunk (LazyList β)
bs.
get: {α : Type v} → Thunk α → α
get)

@[inline] def 
zip: LazyList α → LazyList β → LazyList (α × β)
zip : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type v → Type v
LazyList 
β: Type v
β → 
LazyList: Type (max v u) → Type (max v u)
LazyList (
α: Type u
α × 
β: Type v
β) :=
  
map₂: {α : Type u} → {β : Type v} → {δ : Type (max u v)} → (α → β → δ) → LazyList α → LazyList β → LazyList δ
map₂ 
Prod.mk: {α : Type u} → {β : Type v} → α → β → α × β
Prod.mk

partial def 
join: LazyList (LazyList α) → LazyList α
join : 
LazyList: Type u → Type u
LazyList (
LazyList: Type u → Type u
LazyList 
α: Type u
α) → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
nil: {α : Type ?u.3036} → LazyList α
nil          => 
nil: {α : Type u} → LazyList α
nil
  | 
cons: {α : Type ?u.3047} → α → LazyList α → LazyList α
cons 
a: LazyList α
a 
as: LazyList (LazyList α)
as    => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
append: {α : Type u} → LazyList α → (Unit → LazyList α) → LazyList α
append 
a: LazyList α
a fun _ => 
join: LazyList (LazyList α) → LazyList α
join 
as: LazyList (LazyList α)
as)
  | 
delayed: {α : Type ?u.3102} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList (LazyList α))
as   => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
join: LazyList (LazyList α) → LazyList α
join 
as: Thunk (LazyList (LazyList α))
as.
get: {α : Type u} → Thunk α → α
get)

@[inline] partial def 
bind: {α : Type u} → {β : Type v} → LazyList α → (α → LazyList β) → LazyList β
bind (
x: LazyList α
x : 
LazyList: Type u → Type u
LazyList 
α: Type u
α) (
f: α → LazyList β
f : 
α: Type u
α → 
LazyList: Type v → Type v
LazyList 
β: Type v
β) : 
LazyList: Type v → Type v
LazyList 
β: Type v
β :=
  
join: {α : Type v} → LazyList (LazyList α) → LazyList α
join (
x: LazyList α
x.
map: {α : Type u} → {β : Type v} → (α → β) → LazyList α → LazyList β
map 
f: α → LazyList β
f)

instance: Monad LazyList
instance : 
Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
LazyList: Type u_1 → Type u_1
LazyList where
  pure := 
LazyList.pure: {α : Type u_1} → α → LazyList α
LazyList.pure
  bind := 
LazyList.bind: {α β : Type u_1} → LazyList α → (α → LazyList β) → LazyList β
LazyList.bind
  map  := 
LazyList.map: {α β : Type u_1} → (α → β) → LazyList α → LazyList β
LazyList.map

instance: Alternative LazyList
instance : 
Alternative: (Type u_1 → Type u_1) → Type (u_1 + 1)
Alternative 
LazyList: Type u_1 → Type u_1
LazyList where
  failure := 
nil: {α : Type u_1} → LazyList α
nil
  orElse  := 
LazyList.append: {α : Type u_1} → LazyList α → (Unit → LazyList α) → LazyList α
LazyList.append

partial def 
approx: Nat → LazyList α → List α
approx : 
Nat: Type
Nat → 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
List: Type u → Type u
List 
α: Type u
α
  | 
0: Nat
0,     
as: LazyList α
as
Warning: unused variable `as`           => 
[]: List α
[]
  | _,     
nil: {α : Type ?u.3731} → LazyList α
nil          => 
[]: List α
[]
  | 
i: Nat
i+1,   
cons: {α : Type ?u.3749} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as    => 
a: α
a :: 
approx: Nat → LazyList α → List α
approx 
i: Nat
i 
as: LazyList α
as
  | 
i: Nat
i+1,   
delayed: {α : Type ?u.3839} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
approx: Nat → LazyList α → List α
approx (
i: Nat
i+
1: Nat
1) 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get

partial def 
iterate: (α → α) → α → LazyList α
iterate (
f: α → α
f : 
α: Type u
α → 
α: Type u
α) : 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
x: α
x => 
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
x: α
x (
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
iterate: (α → α) → α → LazyList α
iterate 
f: α → α
f (
f: α → α
f 
x: α
x)))

partial def 
iterate₂: (α → α → α) → α → α → LazyList α
iterate₂ (
f: α → α → α
f : 
α: Type u
α → 
α: Type u
α → 
α: Type u
α) : 
α: Type u
α → 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
x: α
x, 
y: α
y => 
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
x: α
x (
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
iterate₂: (α → α → α) → α → α → LazyList α
iterate₂ 
f: α → α → α
f 
y: α
y (
f: α → α → α
f 
x: α
x 
y: α
y)))

partial def 
filter: (α → Bool) → LazyList α → LazyList α
filter (
p: α → Bool
p : 
α: Type u
α → 
Bool: Type
Bool) : 
LazyList: Type u → Type u
LazyList 
α: Type u
α → 
LazyList: Type u → Type u
LazyList 
α: Type u
α
  | 
nil: {α : Type ?u.4392} → LazyList α
nil          => 
nil: {α : Type u} → LazyList α
nil
  | 
cons: {α : Type ?u.4403} → α → LazyList α → LazyList α
cons 
a: α
a 
as: LazyList α
as    => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (if 
p: α → Bool
p 
a: α
a then 
cons: {α : Type u} → α → LazyList α → LazyList α
cons 
a: α
a (
filter: (α → Bool) → LazyList α → LazyList α
filter 
p: α → Bool
p 
as: LazyList α
as) else 
filter: (α → Bool) → LazyList α → LazyList α
filter 
p: α → Bool
p 
as: LazyList α
as)
  | 
delayed: {α : Type ?u.4545} → Thunk (LazyList α) → LazyList α
delayed 
as: Thunk (LazyList α)
as   => 
delayed: {α : Type u} → Thunk (LazyList α) → LazyList α
delayed (
filter: (α → Bool) → LazyList α → LazyList α
filter 
p: α → Bool
p 
as: Thunk (LazyList α)
as.
get: {α : Type u} → Thunk α → α
get)

end LazyList