mathlib docs: core.data.lazy

source

inductive lazy_list :

Type u → Type u

nil : Π (α : Type u), lazy_list α
cons : Π (α : Type u), α → thunk (lazy_list α) → lazy_list α

source

def lazy_list.singleton {α : Type u} :

α → lazy_list α

Equations

lazy_list.singleton a = lazy_list.cons a (λ («_» : unit), lazy_list.nil)

source

def lazy_list.of_list {α : Type u} :

list α → lazy_list α

Equations

lazy_list.of_list (h :: t) = lazy_list.cons h (λ («_» : unit), lazy_list.of_list t)
lazy_list.of_list list.nil = lazy_list.nil

source

def lazy_list.to_list {α : Type u} :

lazy_list α → list α

Equations

(lazy_list.cons h t).to_list = h :: (t ()).to_list
lazy_list.nil.to_list = list.nil

source

def lazy_list.head {α : Type u} [inhabited α] :

lazy_list α → α

Equations

(lazy_list.cons h t).head = h
lazy_list.nil.head = inhabited.default α

source

def lazy_list.tail {α : Type u} :

lazy_list α → lazy_list α

Equations

(lazy_list.cons h t).tail = t ()
lazy_list.nil.tail = lazy_list.nil

source

def lazy_list.append {α : Type u} :

lazy_list α → thunk (lazy_list α) → lazy_list α

Equations

(lazy_list.cons h t).append l = lazy_list.cons h (λ («_» : unit), (t ()).append l)
lazy_list.nil.append l = l ()

source

def lazy_list.map {α : Type u} {β : Type v} :

(α → β) → lazy_list α → lazy_list β

Equations

lazy_list.map f (lazy_list.cons h t) = lazy_list.cons (f h) (λ («_» : unit), lazy_list.map f (t ()))
lazy_list.map f lazy_list.nil = lazy_list.nil

source

def lazy_list.map₂ {α : Type u} {β : Type v} {δ : Type w} :

(α → β → δ) → lazy_list α → lazy_list β → lazy_list δ

Equations

lazy_list.map₂ f (lazy_list.cons h₁ t₁) (lazy_list.cons h₂ t₂) = lazy_list.cons (f h₁ h₂) (λ («_» : unit), lazy_list.map₂ f (t₁ ()) (t₂ ()))
lazy_list.map₂ f (lazy_list.cons hd tl) lazy_list.nil = lazy_list.nil
lazy_list.map₂ f lazy_list.nil (lazy_list.cons hd tl) = lazy_list.nil
lazy_list.map₂ f lazy_list.nil lazy_list.nil = lazy_list.nil

source

def lazy_list.zip {α : Type u} {β : Type v} :

lazy_list α → lazy_list β → lazy_list (α × β)

Equations

lazy_list.zip = lazy_list.map₂ prod.mk

source

def lazy_list.join {α : Type u} :

lazy_list (lazy_list α) → lazy_list α

Equations

(lazy_list.cons h t).join = h.append (λ («_» : unit), (t ()).join)
lazy_list.nil.join = lazy_list.nil

source

def lazy_list.for {α : Type u} {β : Type v} :

lazy_list α → (α → β) → lazy_list β

Equations

l.for f = lazy_list.map f l

source

def lazy_list.approx {α : Type u} :

ℕ → lazy_list α → list α

Equations

lazy_list.approx (a + 1) (lazy_list.cons h t) = h :: lazy_list.approx a (t ())
lazy_list.approx n.succ lazy_list.nil = list.nil
lazy_list.approx 0 (lazy_list.cons hd tl) = list.nil
lazy_list.approx 0 lazy_list.nil = list.nil

source

def lazy_list.filter {α : Type u} (p : α → Prop) [decidable_pred p] :

lazy_list α → lazy_list α

Equations

lazy_list.filter p (lazy_list.cons h t) = ite (p h) (lazy_list.cons h (λ («_» : unit), lazy_list.filter p (t ()))) (lazy_list.filter p (t ()))
lazy_list.filter p lazy_list.nil = lazy_list.nil

source

def lazy_list.nth {α : Type u} :

lazy_list α → ℕ → option α

Equations

(lazy_list.cons a l).nth (n + 1) = (l ()).nth n
(lazy_list.cons a l).nth 0 = option.some a
lazy_list.nil.nth n = option.none

source

meta def lazy_list.iterates {α : Type u} :

(α → α) → α → lazy_list α

source

meta def lazy_list.iota :

ℕ → lazy_list ℕ

mathlib documentation

core.data.lazy_list

General documentation

Additional documentation

Library

mathlib documentation

core.​data.​lazy_list

General documentation

Additional documentation

Library

core.data.lazy_list