def Sequ (A : Sort u) : Sort u

Equations

• Sequ A = (Nat → A)

def Sequ.cons {A : Sort u_1} (head : A) (tail : Sequ A) : Sequ A

Equations

• (head :: tail) 0 = head
• (head :: tail) n.succ = tail n

def sequ_cons : Lean.TrailingParserDescr

Equations

• sequ_cons = Lean.ParserDescr.trailingNode `sequ_cons 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem Sequ.cons_zero {A : Sort u_1} {hd : A} {tl : Sequ A} : (hd :: tl) 0 = hd

@[simp]

theorem Sequ.cons_succ {A : Sort u_1} {hd : A} {n : Nat} {tl : Sequ A} : (hd :: tl) (n + 1) = tl n

def Sequ.head {A : Sort u_1} (s : Sequ A) : A

Equations

• s.head = s 0

@[simp]

theorem Sequ.head_cons {A✝ : Sort u_1} {hd : A✝} {tl : Sequ A✝} : (hd :: tl).head = hd

def Sequ.tail {A : Sort u_1} (s : Sequ A) : Sequ A

Equations

• s.tail x✝ = s (x✝ + 1)

@[simp]

theorem Sequ.tail_cons {A✝ : Sort u_1} {hd : A✝} {tl : Sequ A✝} : (hd :: tl).tail = tl

def Sequ.uncons {A : Sort u_1} (s : Sequ A) : A ×' Sequ A

Equations

• s.uncons = ⟨s.head, s.tail⟩

@[simp]

theorem Sequ.uncons_cons {A✝ : Sort u_1} {hd : A✝} {tl : Sequ A✝} : (hd :: tl).uncons = ⟨hd, tl⟩

theorem Sequ.uncons_iff {A✝ : Sort u_1} {v : Sequ A✝} {hd : A✝} {tl : Sequ A✝} : v.uncons = ⟨hd, tl⟩ ↔ v = hd :: tl

def Sequ.coiter {A : Sort u_1} {X : Sort u2} (hd : X → A) (tl : X → X) : X → Sequ A

Equations

• Sequ.coiter hd tl x✝ 0 = hd x✝
• Sequ.coiter hd tl x✝ n.succ = Sequ.coiter hd tl (tl x✝) n

@[simp]

theorem Sequ.iter_head {X✝ : Sort u_1} {α✝ : Sort u_2} {hd : X✝ → α✝} {tl : X✝ → X✝} {x : X✝} : (coiter hd tl x).head = hd x

@[simp]

theorem Sequ.iter_tail {X✝ : Sort u_1} {A✝ : Sort u_2} {hd : X✝ → A✝} {tl : X✝ → X✝} {x : X✝} : (coiter hd tl x).tail = coiter hd tl (tl x)

@[simp]

theorem Sequ.fold_id {A : Sort u_1} {v : Sequ A} : (fun (n : Nat) => id (v n)) = v

theorem Sequ.map_compose {A : Sort u_1} {β✝ : Sort u_2} {δ✝ : Sort u_3} {f : β✝ → δ✝} {g : A → β✝} {v : Sequ A} : (fun (n : Nat) => f ((fun (n : Nat) => g (v n)) n)) = fun (n : Nat) => (f ∘ g) (v n)