Solution for task_chapter12 (#7)

* Round 1: Chapter 12 implemented: 941 lines, 11 sections (12.1-12.11), 34 code blocks across 8 env tags, 12 exercises. All MDX tests pass, full build succeeds.

* Remove unmodified feature file task_chapter12.md

* Pre-PR cleanup for task_chapter12

* Address PR feedback: fix leq GADT and VL lens encoding

- Fix unsound leq GADT: use Peano type-level naturals so the Step
  constructor preserves the upper bound type parameter, with a
  working transitivity (composition) proof.
- Fix Van Laarhoven lens: replace single _fst that was specialized
  to Identity with separate get/set demonstrations, and explain
  OCaml's higher-rank limitation.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: lukstafi

AGENTS_STAGING.md

@@ -0,0 +1,14 @@
+# Agent Learnings (Staging)
+
+This file collects agent-discovered learnings for later curation into CLAUDE.md / AGENTS.md.
+
+<!-- Entry: task_chapter12-coder | 2026-02-20 -->
+### Chapter 12 build and MDX gotchas
+
+- **Float.round API**: OCaml's `Float.round` takes only one argument (the float). It does not accept a rounding direction parameter. Use `Float.floor`, `Float.ceil`, or `Float.round` (rounds to nearest even) directly.
+- **MDX env isolation**: Each `env=` tag creates a fully isolated toplevel. The prelude is loaded into every environment, but definitions from one `env=` block are invisible to blocks with a different tag. Plan environment grouping carefully before writing code.
+- **Root dune concatenation**: When adding a new chapter, update both the `deps` list and the `action` body in the root `dune` file's README.md rule. Missing either causes a build failure.
+- **Pipeline assertion values**: When writing test assertions for multi-stage pipelines, trace through each stage manually. A common error is asserting the wrong intermediate count (e.g., counting words after split without accounting for all tokens).
+- **Unicode in code comments**: Characters like `∘`, `≅`, `≠` in OCaml code comments or markdown prose trigger PDF font warnings (`Missing character` from lualatex). These are non-fatal but noisy. Prefer ASCII equivalents in code comments; Unicode is fine in markdown prose where KaTeX/pandoc handles rendering.
+
+<!-- End entry -->

README.md

@@ -0,0 +1,3 @@
+(mdx
+ (files README.md)
+ (preludes prelude.ml))

chapter12/README.md

@@ -0,0 +1,38 @@
+let ( -| ) f g x = f (g x)
+let ( |- ) f g x = g (f x)
+
+module type MONAD = sig
+  type 'a t
+  val return : 'a -> 'a t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+end
+
+module type MONAD_OPS = sig
+  type 'a monad
+  include MONAD with type 'a t := 'a monad
+  val ( let* ) : 'a monad -> ('a -> 'b monad) -> 'b monad
+  val ( let+ ) : 'a monad -> ('a -> 'b) -> 'b monad
+  val ( >>= ) : 'a monad -> ('a -> 'b monad) -> 'b monad
+  val join : 'a monad monad -> 'a monad
+end
+
+module MonadOps (M : MONAD) = struct
+  open M
+  type 'a monad = 'a t
+  let ( let* ) a b = bind a b
+  let ( let+ ) a f = bind a (fun x -> return (f x))
+  let (>>=) a b = bind a b
+  let join m =
+    let* x = m in
+    x
+end
+
+module Monad (M : MONAD) :
+sig
+  include MONAD_OPS
+  val run : 'a monad -> 'a M.t
+end = struct
+  include M
+  include MonadOps(M)
+  let run x = x
+end

chapter12/dune

@@ -15,7 +15,8 @@
   chapter8/README.md
   chapter9/README.md
   chapter10/README.md
-  chapter11/README.md)
+  chapter11/README.md
+  chapter12/README.md)
  (action
   (with-stdout-to
    README.md
@@ -45,7 +46,9 @@
     (echo "\n\n")
     (cat chapter10/README.md)
     (echo "\n\n")
-    (cat chapter11/README.md)))))
+    (cat chapter11/README.md)
+    (echo "\n\n")
+    (cat chapter12/README.md)))))
 
 (rule
  (target old_lectures_as_book.md)