Cancel the third office hours, minor tweaks for third lecture code

Changes

2 changed files (+12/-33)

• MoreBasic.lean
  • @@ -8,11 +8,14 @@ namespace Monad
    #eval [1, 2, 3].map (· * 2) + #eval (· * 2) <$> [1, 2, 3] + + + #eval (some 2).map (· * 2) #eval none.map (· * 2) - #eval (· * 2) <$> [1, 2, 3] #check List.map
  • @@ -22,6 +25,8 @@ #check Except.map
    #check Tree.map + -- #check .map + class Functor' (f : Type → Type) where map : (α → β) → f α → f β
  • @@ -33,7 +38,7 @@ #eval (· * 2) 🤑 [1, 2, 3]
    class LawfulFunctor' f [Functor' f] where id_map (x : f α) : id <$> x = x - comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x + comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> (g <$> x) @[simp] instance : Functor' Option where
  • @@ -45,14 +50,6 @@ instance : LawfulFunctor' Option where
    id_map x := by cases x <;> simp comp_map g h x := by cases x <;> simp - @[simp] - instance (α : Type) : Functor' (α → ·) where - map f g := f ∘ g - - instance (α : Type) : LawfulFunctor' (α → ·) where - id_map := by simp - comp_map := by simp [Function.comp_assoc] - #simp (some 3).map (· * ·)
  • @@ -65,8 +62,11 @@ scoped infixl:60 " <*> " => Applicative'.seq
    class LawfulApplicative' f [Applicative' f] extends LawfulFunctor' f where pure_seq (g : α → β) (x : f α) : pure g <*> x = g <$> x + map_pure (g : α → β) (x : α) : g <$> (pure x : f α) = pure (g x) + seq_pure (g : f (α → β)) (x : α) : g <*> pure x = (· x) <$> g + seq_assoc (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = (· ∘ ·) <$> h <*> g <*> x comp_map g h x := (by repeat rw [← pure_seq]
  • @@ -74,17 +74,6 @@ simp [seq_assoc, map_pure, seq_pure])
    #eval ((· * ·) <$> (Except.ok 3) <*> (Except.ok 4) : Except String ℕ) - @[simp] - instance (α : Type) : Applicative' (α → ·) where - pure x := fun _ ↦ x - seq f g := fun x ↦ f x (g x) - - instance (α : Type) : LawfulApplicative' (α → ·) where - pure_seq := by simp; grind - map_pure := by simp; grind - seq_pure := by simp; grind - seq_assoc := by simp - def one_over (x : ℕ) : Option ℚ := if x = 0 then
  • @@ -92,7 +81,7 @@ none -- Division by 0 is undefined
    else some <| 1 / x - #eval one_over 2 + #eval one_over 42 #eval one_over (some 2)
  • @@ -114,16 +103,6 @@ bind_assoc (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun y ↦ f y >>= g
    map_pure g x := (by rw [← bind_pure_comp, pure_bind]) seq_pure g x := (by simp [← bind_map, map_pure, bind_pure_comp]) seq_assoc x g h := (by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind]) - - @[simp] - instance (α : Type) : Monad' (α → ·) where - bind f g := fun x ↦ g (f x) x - - instance (α : Type) : LawfulMonad' (α → ·) where - bind_pure_comp := by simp; grind - bind_map := by simp - pure_bind := by simp - bind_assoc := by simp @[simp] instance : Monad' Option where
• index.html
  • @@ -26,7 +26,7 @@ </p>
    <hr> <h2>Schedule</h2> <p><b>Location and time:</b> 6-7:30 PM, 3-370</p> - <p><b>Office hours:</b> 3-5 PM, Jan {19, 22, 26}, W20-557 (SIPB office)</p> + <p><b>Office hours:</b> 3-5 PM, Jan {19, 22}, W20-557 (SIPB office)</p> <table> <tr> <th>Date</th>