fix(data/seq): option_bind, option_map -> option.bind, option.map (ch…

…anged in Lean)

data/seq/parallel.lean

@@ -94,7 +94,7 @@ begin
   intro n, induction n with n IH; intros l S c o T,
   { cases o, { exact terminates_parallel.aux a T },
     have H : seq.destruct S = some (some c, _),
-    { unfold seq.destruct has_map.map, rw ←a, simp [option_map, option_bind] },
+    { unfold seq.destruct has_map.map, rw ←a, simp [option.map, option.bind] },
     ginduction (parallel.aux2 l) with h a l';
     have C : corec parallel.aux1 (l, S) = _,
     { apply destruct_eq_ret, simp [parallel.aux1], rw [h], simp [rmap] },

data/seq/seq.lean

@@ -74,7 +74,7 @@ begin
   dsimp [destruct],
   ginduction nth s 0 with f0 a'; intro h,
   { contradiction },
-  { unfold has_map.map at h, dsimp [option_map, option_bind] at h,
+  { unfold has_map.map at h, dsimp [option.map, option.bind] at h,
     cases s with f al,
     injections with _ h1 h2,
     rw ←h2, apply subtype.eq, dsimp [tail, cons],
@@ -154,7 +154,7 @@ begin
   change stream.corec' (corec.F f) (some b) 0 with (corec.F f (some b)).1,
   unfold has_map.map, dsimp [corec.F],
   ginduction f b with h s, { refl },
-  cases s with a b', dsimp [corec.F, option_bind],
+  cases s with a b', dsimp [corec.F, option.bind],
   apply congr_arg (λ b', some (a, b')),
   apply subtype.eq,
   dsimp [corec, tail],
@@ -259,7 +259,7 @@ def append (s₁ s₂ : seq α) : seq α :=
   end) (s₁, s₂)
 
 def map (f : α → β) : seq α → seq β | ⟨s, al⟩ :=
-⟨s.map (option_map f),
+⟨s.map (option.map f),
 λn, begin
   dsimp [stream.map, stream.nth],
   ginduction s n with e; intro,
@@ -402,7 +402,7 @@ begin
   end end
 end
 
-@[simp] theorem map_nth (f : α → β) : ∀ s n, nth (map f s) n = option_map f (nth s n)
+@[simp] theorem map_nth (f : α → β) : ∀ s n, nth (map f s) n = (nth s n).map f
 | ⟨s, al⟩ n := rfl
 
 instance : functor seq :=
@@ -502,7 +502,7 @@ begin
 end
 
 theorem mem_map (f : α → β) {a : α} : ∀ {s : seq α}, a ∈ s → f a ∈ map f s
-| ⟨g, al⟩ := stream.mem_map (option_map f)
+| ⟨g, al⟩ := stream.mem_map (option.map f)
 
 theorem exists_of_mem_map {f} {b : β} : ∀ {s : seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
 | ⟨g, al⟩ h := let ⟨o, om, oe⟩ := stream.exists_of_mem_map h in

data/seq/wseq.lean

@@ -245,7 +245,7 @@ def collect (s : wseq α) (n : ℕ) : list α :=
 
 def append : wseq α → wseq α → wseq α := seq.append
 
-def map (f : α → β) : wseq α → wseq β := seq.map (option_map f)
+def map (f : α → β) : wseq α → wseq β := seq.map (option.map f)
 
 def join (S : wseq (wseq α)) : wseq α :=
 seq.join ((λo : option (wseq α), match o with
@@ -885,13 +885,13 @@ theorem to_list_of_list (l : list α) : l ∈ to_list (of_list l) :=
 by induction l with a l IH; simp [ret_mem]; exact think_mem (mem_map _ IH)
 
 @[simp] theorem destruct_of_seq (s : seq α) :
-  destruct (of_seq s) = return (option_map (λ a, (a, of_seq s.tail)) s.head) :=
+  destruct (of_seq s) = return (s.head.map $ λ a, (a, of_seq s.tail)) :=
 destruct_eq_ret $ begin
   simp [of_seq, head, destruct, seq.destruct, seq.head],
   rw [show seq.nth (some <$> s) 0 = some <$> seq.nth s 0, by apply seq.map_nth],
   cases seq.nth s 0 with a, { refl },
   unfold has_map.map,
-  simp [option_map, option_bind, destruct]
+  simp [option.map, option.bind, destruct]
 end
 
 @[simp] theorem head_of_seq (s : seq α) : head (of_seq s) = return s.head :=
@@ -946,7 +946,7 @@ begin
 end
 
 theorem mem_map (f : α → β) {a : α} {s : wseq α} : a ∈ s → f a ∈ map f s :=
-seq.mem_map (option_map f)
+seq.mem_map (option.map f)
 
 -- The converse is not true without additional assumptions
 theorem exists_of_mem_join {a : α} : ∀ {S : wseq (wseq α)}, a ∈ join S → ∃ s, s ∈ S ∧ a ∈ s :=
@@ -983,10 +983,10 @@ let ⟨t, tm, bt⟩ := exists_of_mem_join h,
     ⟨a, as, e⟩ := exists_of_mem_map tm in ⟨a, as, by rwa e⟩
 
 theorem destruct_map (f : α → β) (s : wseq α) :
-  destruct (map f s) = computation.map (option_map (prod.map f (map f))) (destruct s) :=
+  destruct (map f s) = computation.map (option.map (prod.map f (map f))) (destruct s) :=
 begin
   apply eq_of_bisim (λ c1 c2, ∃ s, c1 = destruct (map f s) ∧
-    c2 = computation.map (option_map (prod.map f (map f))) (destruct s)),
+    c2 = computation.map (option.map (prod.map f (map f))) (destruct s)),
   { intros c1 c2 h, cases h with s h, rw [h.left, h.right],
     apply s.cases_on _ (λ a s, _) (λ s, _); simp; simp,
     { refl }, { refl }, { exact ⟨s, rfl, rfl⟩ } },
@@ -1003,7 +1003,7 @@ theorem lift_rel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop)
 λ s1 s2 h, match s1, s2, h with ._, ._, ⟨s, t, rfl, rfl, h⟩ := begin
   simp [destruct_map], apply computation.lift_rel_map _ _ (lift_rel_destruct h),
   intros o p h,
-  cases o with a; cases p with b; simp [option_map, option_bind],
+  cases o with a; cases p with b; simp [option.map, option.bind],
   { cases b; cases h },
   { cases a; cases h },
   { cases a with a s; cases b with b t, cases h with r h,