Chapters 10 and 13

Fad/API.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2025 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sorrachai Yingchareonthawornchai
+-/
+
+import Mathlib.Tactic -- imports all of the tactics in Lean's maths library
+
+
+set_option autoImplicit false
+set_option tactic.hygienic false
+
+structure TimeM (α : Type) where
+  ret : α
+  time : ℕ
+
+namespace TimeM
+
+def pure {α} (a : α) : TimeM α :=
+  ⟨a, 0⟩
+
+def bind {α β} (m : TimeM α) (f : α → TimeM β) : TimeM β :=
+  let r := f m.ret
+  ⟨r.ret, m.time + r.time⟩
+
+instance : Monad TimeM where
+  pure := pure
+  bind := bind
+
+-- Increment time
+@[simp] def tick {α : Type} (a : α) (c : ℕ := 1) : TimeM α :=
+  ⟨a, c⟩
+
+notation "✓" a:arg ", " c:arg => tick a c
+notation "✓" a:arg => tick a  -- Default case with only one argument
+
+def tickUnit : TimeM Unit :=
+  ✓ () -- This uses the default time increment of 1
+
+@[grind, simp] theorem time_of_pure {α} (a : α) : (pure a).time = 0 := rfl
+@[grind, simp] theorem time_of_bind {α β} (m : TimeM α) (f : α → TimeM β) :
+ (TimeM.bind m f).time = m.time + (f m.ret).time := rfl
+@[grind, simp] theorem time_of_tick {α} (a : α) (c : ℕ) : (tick a c).time = c := rfl
+@[grind, simp] theorem ret_bind {α β} (m : TimeM α) (f : α → TimeM β) :
+  (TimeM.bind m f).ret = (f m.ret).ret := rfl
+
+-- allow us to simplify the chain of compositions
+attribute [simp] Bind.bind Pure.pure TimeM.pure
+
+
+end TimeM