@[instance]
Equations
- lazy_list.list_equiv_lazy_list α = {to_fun := lazy_list.of_list α, inv_fun := lazy_list.to_list α, left_inv := _, right_inv := _}
@[instance]
Equations
@[instance]
Equations
- lazy_list.decidable_eq (lazy_list.cons x xs) (lazy_list.cons y ys) = dite (x = y) (λ (h : x = y), lazy_list.decidable_eq._match_1 x xs y ys h (lazy_list.decidable_eq (xs ()) (ys ()))) (λ (h : ¬x = y), decidable.is_false _)
- lazy_list.decidable_eq (lazy_list.cons _x _x_1) lazy_list.nil = decidable.is_false _
- lazy_list.decidable_eq lazy_list.nil (lazy_list.cons _x _x_1) = decidable.is_false _
- lazy_list.decidable_eq lazy_list.nil lazy_list.nil = decidable.is_true lazy_list.decidable_eq._main._proof_1
- lazy_list.decidable_eq._match_1 x xs y ys h (decidable.is_true h2) = have this : xs = ys, from _, decidable.is_true _
- lazy_list.decidable_eq._match_1 x xs y ys h (decidable.is_false h2) = decidable.is_false _
Equations
- lazy_list.traverse f (lazy_list.cons x xs) = lazy_list.cons <$> f x <*> thunk.mk <$> lazy_list.traverse f (xs ())
- lazy_list.traverse f lazy_list.nil = has_pure.pure lazy_list.nil
@[instance]
Equations
- lazy_list.traversable = {to_functor := {map := lazy_list.traverse monad.to_applicative, map_const := λ (α β : Type u_1), lazy_list.traverse ∘ function.const β}, traverse := lazy_list.traverse}
@[instance]
Equations
- lazy_list.is_lawful_traversable = equiv.is_lawful_traversable' lazy_list.list_equiv_lazy_list lazy_list.is_lawful_traversable._proof_1 lazy_list.is_lawful_traversable._proof_2 lazy_list.is_lawful_traversable._proof_3