LazyList.cons.injEq
theorem LazyList.cons.injEq :
∀ {α : Type u} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
(LazyList.cons hd tl = LazyList.cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
This theorem states that for any type `α`, and any two pairs of head elements (`hd` and `hd_1`) and thunk of lazy lists (`tl` and `tl_1`) of type `α`, the equality of two constructed lazy lists with these elements is equivalent to the equality of both the head elements and the thunk of lazy lists. In other words, two lazy lists are equal if and only if their head elements are equal and their thunk of tail lists are equal.
More concisely: For any type `α`, two constructed lazy lists `[h₁ : α] :: tl₁ : lazy list α` and `[h₂ : α] :: tl₂ : lazy list α` are equal if and only if `h₁ = h₂` and `tl₁ = tl₂`.
|
LazyList.cons.sizeOf_spec
theorem LazyList.cons.sizeOf_spec :
∀ {α : Type u} [inst : SizeOf α] (hd : α) (tl : Thunk (LazyList α)),
sizeOf (LazyList.cons hd tl) = 1 + sizeOf hd + sizeOf tl
This theorem is about the size of a lazy list in Lean 4, which is a type of list where the tail is computed on demand. Specifically, it states that for any type `α` that has a defined `SizeOf` instance (which gives the size of an object of that type), and for any head element `hd` of type `α` and tail `tl` of type `Thunk (LazyList α)`, the size of the lazy list constructed with `LazyList.cons hd tl` is equal to `1` (for the cons cell itself) plus the size of the head element `hd` plus the size of the tail `tl`.
More concisely: The size of a lazy list `LazyList.cons hd tl` in Lean 4, where `hd` is of type `α` with a defined `SizeOf` instance and `tl` is of type `Thunk (LazyList α)`, is equal to 1 + `SizeOf hd` + `SizeOf tl`.
|