Remove extra dots

Changes

1 changed files (+8/-8)

• lazy.lean
  • @@ -40,17 +40,17 @@ inductive LazyList (α : Type u) where
    def LazyList.take : Nat → LazyList α → List α | 0, _ => .nil - | _, .nil => .nil - | n + 1, .cons x xs => .cons x <| xs.get.take n + | _, nil => .nil + | n + 1, cons x xs => .cons x <| xs.get.take n def LazyList.map (f: α → β) : LazyList α → LazyList β - | .nil => .nil - | .cons x xs => .cons (f x) <| xs.get.map f + | nil => nil + | cons x xs => cons (f x) <| xs.get.map f def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ - | .nil, _ => .nil - | _, .nil => .nil - | .cons x xs, .cons y ys => .cons (f x y) <| zipWith f xs.get ys.get + | nil, _ => nil + | _, nil => nil + | cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get unsafe def ints := LazyList.cons 1.0 <| ints.map (· + 1)
  • @@ -78,7 +78,7 @@ end
    #eval sine.take 10 - #eval evalAt 100 sine 2.0 + #eval evalAt 1000 sine 2.0 #eval 2.0.sin -- inductive LazyList (α : Type u) where