diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
new file mode 100644
index 0000000..0a36a59
--- /dev/null
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -0,0 +1,77 @@
+# Lessons
+
+Append-only log, newest at the bottom. Each entry: what happened, what it cost, what to do
+differently. A line marked **rule** is binding on the next run until it is folded into SKILL.md,
+brief.md or workflow.js and deleted here. Keep the calibration table current.
+
+## Calibration
+
+| knob | value | why |
+|---|---|---|
+| hedgehog (Scala) | `qa.hedgehog::hedgehog-core:0.14.0`, `hedgehog-runner:0.14.0` | 0.13.0 is refused by scala-cli's outdated-dep check |
+| Scala | 3.3.4 via scala-cli 1.12.x | matches the site's other Scala |
+| Haskell | GHC 9.8.4 + hedgehog, docker image `cp-hedgehog` | no host ghc; nix store is read-only |
+| `cp-hedgehog` build | ~2.5 min (cabal update + install --lib hedgehog) | one-off per machine |
+| test count | 100 default; **500** when a property has an equality boundary | measured: 100 tests missed `<` vs `<=` mutants 60–90% of the time |
+| generator ranges | narrow (−30..30, limits 0..20) for boundary-heavy code; full `Int` only in adversarial probes | narrow ranges hit `next == -limit` often; wide ones almost never |
+| pane width | source lines ≤ 72 chars | 77-char comment lines overflowed a 608px pane at 0.78rem mono |
+| workflow | 22 agents, ≈ 65 min wall-clock over two runs (12 min to the first crash + 53 min resumed); the reviewer's mutation + probe round is the long pole (≈ 15–20 min) | extract-method, 2026-09-03 |
+
+## 2026-09-03 — 01 Extract method (first entry; the skill was extracted from this run)
+
+- **Toolchain.** No ghc on the host; `nix shell`/`nix-shell` fail (registry needs network config; store is
+  read-only). `docker run haskell:9.8-slim` + `cabal install --lib hedgehog` works; baked into `cp-hedgehog`
+  and into run.sh's fallback. scala-hedgehog 0.14.0: `Test.renderReport(..., ansiCodesSupported = false)`;
+  `object Props extends Properties` brings its own main, so run with `--main-class spec`.
+- **Reviewer, round 1 (blocking).** Example 02's generators were too weak: mutants `tx < 0 → tx <= 0` and
+  `next < -limit → next <= -limit` survived most runs in both languages. Cause: wide ranges (−500..500)
+  rarely hit the equality boundary and `fee = 0` hides the fee branch. Fix: ranges −30..30 / 0..20 / fee
+  1..20 and `withTests 500`; both mutants then caught 10/10. → became the generator rules in brief.md.
+- **Reviewer, round 1 (optional, applied).** Haskell Before had the step as a `where` binding while Scala
+  had an inline lambda; the two Befores were not parallel. Rewritten as an inline lambda. → rule in brief.
+- **Reviewer, round 2 (optional, applied).** Comment "never throws" overclaimed: GHC `div` overflows at
+  `minBound / -1`. Reworded, and the page says the partiality is preserved, not fixed. `foldl` → `foldl'`.
+- **Citation skeptic.** One of 15 references was refuted on its *claim*, not its existence: "spends most of
+  its effort on this analysis" about Stocker's Scala refactoring thesis was not supported; softened to
+  "must perform exactly this analysis". → skeptic prompt now names overstatement as a failure.
+- **Harness.** A session limit killed the reviewer mid-run; `Workflow({scriptPath, resumeFromRunId})`
+  replayed the 18 finished agents from cache and re-ran only the reviewer. Cached agents may return empty
+  results; read `journal.jsonl` first.
+- **Jekyll.** `exclude:` the sources dir in `_config.yml`; `include_relative` still reads excluded files.
+  `{% highlight scala %}{% include_relative … %}{% endhighlight %}` works inside raw HTML `<div>`s, so the
+  side-by-side panes need no `markdown="1"`. Dot-dirs (`.scala-build`, `.bsp`) are ignored by Jekyll
+  automatically. Two 80-column panes do not fit the 68ch prose measure; `.rf-pair` bleeds to
+  `min(100vw - 3rem, 1360px)` on ≥1000px viewports.
+- **Time.** Research + 15 citation checks ran in parallel with the examples build (both ≈ 10 min); the
+  reviewer's two rounds plus the fix took most of the 53-minute resumed run; diagrams with browser
+  render-checks ≈ 15 min. Toolchain probing before the workflow cost ≈ 10 min the first time. The main
+  agent used the wait to write the page and check the layout in a scratch build — do the same.
+- **Browser contention.** The diagram agent and the main agent share one Chrome; resize/reload calls on
+  the main agent's tab hang for minutes while the other is screenshotting. Do layout screenshots before
+  the Diagrams phase starts, or after it ends.
+
+## 2026-09-03 — 01 Extract method renamed to "Extract / Inline method" (post-PR-12 review round 3)
+
+- **Reviewer (kryptt).** Rename the entry to "Extract / Inline Method" and add a first **Motivation** section
+  stating why you would go in either direction: duplication and long methods drive Extract; speculative
+  generality and coupling drive Inline. Also (skill-wide): Motivation is always the first section of an entry,
+  and every entry shows up with its dual. → folded into SKILL.md §3 (page section order + the always-first
+  Motivation section with the two-direction motivators), brief.md, and the workflow.js research prompt
+  (Motivation heading, first, with the same motivator guidance). Reference page updated: title, subtitle, intro,
+  new Motivation section.
+
+- **Rule.** Prompt-forced page structure in workflow.js: the research prompt now enumerates the exact H2
+  headings in order with Motivation first — check that list whenever a section is added or renamed, or the
+  assemble-the-page step and the research step will disagree on shape.
+
+## 2026-09-03 — Reference citations are links (post-PR-12 review round 6)
+
+- **Reviewer (kryptt).** In-text `[n]` references must be links that navigate to the reference list.
+  Also update the skill with this info. Implemented:
+  - In-text citations → `[[n](#ref-n)]`, rendering as [<a href="#ref-n">n</a>].
+  - Reference list items → raw HTML `<li id="ref-N">…</li>` inside a plain `<ol>`.
+- **Kramdown traps (rule).** Kramdown 1.x will not process markdown inside raw block HTML (`<li>`, even
+  with `markdown="1"` — it escapes the inner tags); IALs on numbered list items (`{: #ref-N}` on a line
+  after the item) attach to the *enclosing* `<ol>` at a break point and split the list. The working
+  pattern is: a single `<ol>` with raw `<li id="ref-N">` items, and hand-render inline markdown to
+  `<em>`/`<a>` yourself. Folded into SKILL.md §3, workflow.js research prompt, and brief.md.
diff --git a/.claude/skills/refactoring-entry/SKILL.md b/.claude/skills/refactoring-entry/SKILL.md
new file mode 100644
index 0000000..a5f3bbe
--- /dev/null
+++ b/.claude/skills/refactoring-entry/SKILL.md
@@ -0,0 +1,114 @@
+---
+name: refactoring-entry
+description: Add one entry to the Constructive Programming refactoring catalogue at /refactorings/ — research with verified citations, 3 Before/After examples in Scala 3 and Haskell, hedgehog property-based proof of equivalence, diagrams, page, PR. Use when asked to "do the next refactoring", "add <name> to the catalogue", or "write the <name> entry".
+---
+
+# Refactoring catalogue entry
+
+One entry = one refactoring from `_data/refactorings.yml`, read as an equation between programs
+and *checked* with property-based tests. The reference implementation is `/refactorings/extract-method/`
+(page `pages/refactorings/extract-method.md`, sources `pages/refactorings/extract-method/`).
+Copy its shape; do not redesign it.
+
+Each entry is written **with its dual**: the refactoring and its inverse are one equation, and the
+page presents both directions ("Extract / Inline", "Replace X with Y / Replace Y with X"). The list name
+in `_data/refactorings.yml` carries both sides, e.g. `Extract / Inline method`.
+
+## 0. Read the lessons first
+
+Read `LESSONS.md` in this directory, top to bottom. It is the memory of every previous entry: what
+the reviewer caught, what broke, what the calibration table says. Anything marked **rule** there
+overrides the defaults below. If a lesson has become permanent, it has already been folded into
+the steps below and the `workflow.js` prompts; if you find one that has not, fold it in now.
+
+## 1. Set up
+
+1. Branch from `master`: `refactoring/<slug>`.
+2. Pick the entry: the first item in `_data/refactorings.yml` without a `slug`, unless the user
+   names one. Add `slug: <slug>` to it (that is what links it on the index page).
+3. Toolchain check (the workflow agents assume these work):
+   - `scala-cli --version` (hedgehog `qa.hedgehog::hedgehog-core:0.14.0` + `hedgehog-runner:0.14.0`).
+   - `docker image inspect cp-hedgehog` — if missing, `sh pages/refactorings/extract-method/run.sh`
+     builds it (about 2.5 minutes). GHC is not installed on the host; nix is read-only.
+4. Write the brief to the scratchpad: copy `brief.md` from this directory, fill the `<...>` fields.
+   The workflow agents read the brief, not this file.
+
+## 2. Run the workflow (research ∥ examples → verify loop → diagrams)
+
+```
+Workflow({
+  scriptPath: ".claude/skills/refactoring-entry/workflow.js",
+  args: {
+    slug: "<slug>", name: "<Name>", number: <n>, total: 35,
+    brief: "<abs path to brief.md>", scratch: "<abs scratchpad dir>",
+    repo: "<abs repo root>",
+    seeds: ["<paper or tool that anchors the OO side>", "<the FP-side paper>", ...],
+    examples: ["<example 1 idea>", "<example 2 idea>", "<example 3 idea>"]
+  }
+})
+```
+
+- The script runs two tracks in parallel: **research → per-citation skeptics → fix-up**, and
+  **examples → reviewer (mutation + adversarial probes) → fix, up to 3 rounds → diagrams**.
+- If an agent dies (session limit, API error), relaunch with `resumeFromRunId`; finished agents replay
+  from cache. Read `journal.jsonl` before assuming a result is empty.
+- While it runs: write `pages/refactorings/<slug>.md` from the extract-method page (next step), and
+  build the site in a scratch copy with stub SVGs to catch Liquid errors early.
+
+## 3. Assemble the page
+
+Start from `pages/refactorings/extract-method.md`. Keep: front matter shape (`layout: page`,
+`subtitle` carries the koan and names both directions, `permalink: /refactorings/<slug>/`, `tags`,
+`hide: true` so entry pages stay out of the top-right nav), the crumb line, the
+section order (Motivation · The move · To and from + koan figure ·
+Three examples · Pitfalls + a collapsible "The functional reading" footnote ·
+Verification · References) — **Motivation is always
+the first section, before The move** — the `rf-pair` /
+`rf-figure` / `rf-spec` markup, and the `run.sh` instructions. Replace the prose with
+`<scratch>/research.md` (after its citation fix-up) and write one paragraph per example from
+the examples agent's `what_changes` notes.
+
+Motivation states why you would move in either direction: what smell drives the move, and
+what smell drives its inverse. Extract-style motivators include duplication and methods that
+have grown too long; inline-style motivators include speculative generality and coupling
+through a seam's implementation rather than its contract. Two short paragraphs, one per
+direction, before any mechanics — the reader should know when to reach for the move before
+how to perform it.
+
+Rules that came from review, keep them:
+- In-text citations are links: write `[[n](#ref-n)]` (render → [<a href="#ref-n">n</a>]);
+  each reference list item is raw HTML `<li id="ref-N">…</li>` inside a plain `<ol>`, with
+  markdown inline formatting hand-rendered to `<em>` and `<a href>` (Kramdown will not process
+  markdown inside raw block HTML, and IALs on numbered items break the list).
+- Source lines ≤ 72 characters or the pane scrolls horizontally on a 1280px screen.
+- No `{{` `}}` `{%` `%}` in any included source (Liquid runs before highlighting).
+- Copy `run.sh` from extract-method unchanged into the new sources directory.
+- Add the new sources directory to `exclude:` in `_config.yml` (sources are included via
+  `include_relative`, not published as static files).
+- Do not claim totality or purity the code does not have (e.g. `Int` `div` overflow).
+
+## 4. Verify before the PR
+
+1. `sh pages/refactorings/<slug>/run.sh` ends with `all properties passed` — run it yourself, do
+   not trust the agent's report alone.
+2. `bundle exec jekyll build --destination <scratch>/site` exits 0; open the page over
+   `python3 -m http.server` and screenshot at 1280 and 390 wide; no horizontal page scroll,
+   diagrams legible in light and dark.
+3. Re-read the reviewer's last report; every **blocking** item is fixed, every optional item is
+   either applied or deliberately declined in the PR description.
+
+## 5. Ship
+
+Commit sources + page + data + config on the branch; push (SSH remote works; if `gh auth status`
+fails ask the user to run `! gh auth login -h github.com -p ssh -w`); open the PR with the
+reviewer's mutation table and probe summary in the body. The PR preview URL is
+`https://www.constructive.dev/pr-preview/pr-<N>/refactorings/<slug>/`.
+
+## 6. Improve the skill (mandatory, last)
+
+Append a dated entry to `LESSONS.md` with: reviewer findings (blocking and optional), toolchain
+failures and their fixes, wall-clock and agent count from the workflow result, anything the
+prose reviewers (citation skeptics) refuted, and any generator/test-count calibration that
+changed. Then act on it: if a lesson is a rule, edit the rule into this file or into the prompts
+in `workflow.js` so the next run does not have to rediscover it; if a lesson retires an older one,
+delete the older one. Commit the skill change in the same PR.
diff --git a/.claude/skills/refactoring-entry/brief.md b/.claude/skills/refactoring-entry/brief.md
new file mode 100644
index 0000000..cb78550
--- /dev/null
+++ b/.claude/skills/refactoring-entry/brief.md
@@ -0,0 +1,88 @@
+# Brief: "<Name>" — entry <n> of the Constructive Programming refactoring catalogue
+
+## Context
+- Repo: <repo root> (Jekyll site for www.constructive.dev), branch `refactoring/<slug>`.
+- Section: /refactorings/ (index at pages/refactorings.md, list in _data/refactorings.yml). This entry lives at
+  /refactorings/<slug>/ (page pages/refactorings/<slug>.md, sources pages/refactorings/<slug>/).
+- Reference entry, copy its shape exactly: pages/refactorings/extract-method.md and pages/refactorings/extract-method/.
+- Methodology framing (pages/about.md): Constructive Programming = restrictions that make code easier to reason about:
+  referential transparency, totality, termination; Curry–Howard–Lambek. Refactorings are read as *equivalences between
+  programs* that you can state and CHECK — hence property-based tests proving before == after.
+- Audience: senior engineers and CTOs who know OO refactoring (Fowler) and want the typed-FP reading of it.
+- Every entry is presented "to & from": the move AND its inverse (<Name> <-> <inverse name>). The catalogue name
+  carries both sides ("Extract / Inline method"), so does the page title and subtitle; the two directions are
+  one equation.
+
+## This refactoring
+Every entry carries the structure: Motivation first, then the move, the
+functional reading (a collapsible footnote inside Pitfalls), to & from,
+examples, pitfalls, verification, references. Fill the fields below; omit one
+when it does not apply.
+- OO reading: <one paragraph: what the OO/imperative world calls it, where it is catalogued — ONLY when
+  one exists; many moves (higher-order, higher-kinded, dependent-typed) have no OO counterpart, and for
+  those the OO reading is dropped entirely>
+- FP reading: <one paragraph: what it is in a referentially transparent language; which papers/transformations>
+- Dual: <the reverse move — ALWAYS present. Every refactoring is presented as a pair: extract / inline
+  method, introduce / eliminate generics, ... The catalogue name, page title and subtitle carry both
+  sides; the two directions are one equation>
+- Motivation (page section 1, before any mechanics): <why go in each direction — the smell that drives the move,
+  the smell that drives its inverse (e.g. duplication / long methods vs speculative generality / coupling)>
+- Known anchors to verify and cite (find more; verify all): <list>
+- References render as raw HTML: each item is `<li id="ref-N">…</li>` inside a plain `<ol>` (Kramdown
+  won't run markdown inside raw block HTML, so inline `*em*` → `<em>` and `<url>` → `<a href>` by hand).
+  In-text citations are the links `[[n](#ref-n)]`.
+- Example ideas (adjust if you find better, keep the progression simple → free variables/effects → recursion/laziness):
+  1. <...>
+  2. <...>
+  3. <...>
+
+## Code layout (examples agent writes these; reviewer runs them)
+pages/refactorings/<slug>/
+  run.sh                      # copied unchanged from extract-method; runs every NN-*/ dir in both languages
+  NN-<ex>/Before.scala        # object Before { ... }   the pre-refactoring program
+  NN-<ex>/After.scala         # object After  { ... }   the refactored version (same public entry point signature)
+  NN-<ex>/Spec.scala          # hedgehog property: forAll generated inputs, Before.f(x) ==== After.f(x). `@main def spec()`.
+  NN-<ex>/Before.hs           # module Before where ...
+  NN-<ex>/After.hs            # module After  where ...
+  NN-<ex>/Spec.hs             # hedgehog property, main :: IO (); exit non-zero on failure
+- The web page `include_relative`s these files verbatim into highlighted panes, so:
+  * every file self-contained, readable, SHORT (Before/After 8–25 lines each); lines ≤ 72 characters;
+  * NO `{{`, `}}`, `{%`, `%}` sequences anywhere (Liquid would eat them);
+  * one-line comment at the top of Before/After saying what the program does; no essay comments;
+  * the Scala and Haskell Befores must be parallel (same shape: if Scala has an inline lambda, so does Haskell).
+- Scala: Scala 3.3.x, directives at the top of Spec.scala only:
+    //> using scala 3.3.4
+    //> using dep qa.hedgehog::hedgehog-core:0.14.0
+    //> using dep qa.hedgehog::hedgehog-runner:0.14.0
+  Run: `scala-cli run pages/refactorings/<slug>/NN-ex --main-class spec`  (Properties has its own main; name ours `spec`)
+  Known-good hedgehog 0.14.0 runner (renderReport's 4th param is `ansiCodesSupported`):
+    import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+    object Props extends Properties:
+      def tests: List[Test] = List(property("name", prop))
+      def prop: Property = for x <- Gen.int(Range.linear(-100, 100)).forAll yield Before.f(x) ==== After.f(x)
+    @main def spec(): Unit =
+      val results = Props.tests.map { t =>
+        val r = Property.check(t.withConfig(PropertyConfig.default), t.result, Seed.fromTime())
+        println(Test.renderReport("Props", t, r, ansiCodesSupported = false)); r.status }
+      if !results.forall(_ == Status.ok) then sys.exit(1)
+  `.withTests(500)` on a property raises its count.
+- Haskell: GHC 9.8.4 + hedgehog. No ghc on this machine; docker image `cp-hedgehog` (run.sh builds it if missing):
+    docker run --rm -v "$PWD/pages/refactorings/<slug>:/w" -w /w cp-hedgehog runghc -iNN-ex NN-ex/Spec.hs
+  (from the repo root). Spec.hs: `main = do ok <- checkParallel (Group "Props" [...]); unless ok exitFailure`.
+  `withTests 500 $ property $ do ...` raises the count. Prefer `foldl'` over `foldl` for strict accumulators.
+- Run everything at once: `sh pages/refactorings/<slug>/run.sh` (from anywhere).
+
+## Generators (from LESSONS.md — the reviewer will mutation-test them)
+- Design generators around the program's boundaries (equality tests, zero, empty, sign changes): small ranges
+  (e.g. -30..30) hit boundaries far more often than wide ones; exclude values that make a branch invisible
+  (e.g. fee = 0). Use 500 tests when a boundary matters.
+- A second property per example is expected when natural (the extracted piece on its own; a law it obeys).
+- In Haskell probe laziness/strictness with `undefined` where the refactoring could change what is forced;
+  in Scala reason about evaluation count (def vs val, by-name) and say so in a comment when it matters.
+
+## Style
+- Site prose: crisp, editorial, no hype; sentences, not bullets, in body text (the caveats section may use a list).
+- Claims about tools and papers must be modest and literally supported by the cited source.
+- Code: idiomatic, set in a very common domain subject matter, and just enough code to get the point
+  across — no accidental complexity, no clever tricks; the refactoring must be the only difference
+  between Before and After.
diff --git a/.claude/skills/refactoring-entry/workflow.js b/.claude/skills/refactoring-entry/workflow.js
new file mode 100644
index 0000000..88a2ce2
--- /dev/null
+++ b/.claude/skills/refactoring-entry/workflow.js
@@ -0,0 +1,186 @@
+export const meta = {
+  name: 'refactoring-entry',
+  description: 'Research, build, and PBT-verify one refactoring catalogue entry (Scala 3 + Haskell hedgehog)',
+  phases: [
+    { title: 'Research', detail: 'text + references, to & from direction' },
+    { title: 'Citations', detail: 'adversarially verify every reference' },
+    { title: 'Examples', detail: '3 examples, Before/After/Spec in both languages' },
+    { title: 'Verify', detail: 'reviewer runs hedgehog, mutation-tests the specs' },
+    { title: 'Diagrams', detail: 'inline SVG per example + koan' },
+  ],
+}
+
+// args: { slug, name, number, total, brief, scratch, repo, seeds: [...], examples: [...] }
+const A = args
+const BRIEF = A.brief
+const SCRATCH = A.scratch
+const REPO = A.repo
+const EX = `${REPO}/pages/refactorings/${A.slug}`
+const SEEDS = (A.seeds || []).map(s => `- ${s}`).join('\n') || '- (none given; find the primary sources yourself)'
+const EXAMPLE_IDEAS = (A.examples || []).map((e, i) => `  0${i + 1}: ${e}`).join('\n')
+
+const REF = {
+  type: 'object',
+  required: ['id', 'title', 'authors', 'year', 'venue', 'url', 'claim'],
+  properties: {
+    id: { type: 'string' }, title: { type: 'string' }, authors: { type: 'string' },
+    year: { type: 'string' }, venue: { type: 'string' }, url: { type: 'string' },
+    claim: { type: 'string', description: 'what the text attributes to this reference' },
+  },
+}
+const RESEARCH_SCHEMA = {
+  type: 'object', required: ['file', 'references', 'summary'],
+  properties: { file: { type: 'string' }, references: { type: 'array', items: REF }, summary: { type: 'string' } },
+}
+const CITE_SCHEMA = {
+  type: 'object', required: ['id', 'ok', 'note'],
+  properties: { id: { type: 'string' }, ok: { type: 'boolean' }, note: { type: 'string' }, fixed_url: { type: 'string' }, fixed_citation: { type: 'string' } },
+}
+const EXAMPLES_SCHEMA = {
+  type: 'object', required: ['examples', 'notes'],
+  properties: {
+    examples: { type: 'array', items: { type: 'object', required: ['dir', 'title', 'what_changes', 'scala_ok', 'haskell_ok', 'output_tail'],
+      properties: { dir: { type: 'string' }, title: { type: 'string' }, what_changes: { type: 'string' }, scala_ok: { type: 'boolean' }, haskell_ok: { type: 'boolean' }, output_tail: { type: 'string' } } } },
+    notes: { type: 'string' },
+  },
+}
+const VERIFY_SCHEMA = {
+  type: 'object', required: ['passed', 'examples', 'adversarial_findings', 'report_file'],
+  properties: {
+    passed: { type: 'boolean' },
+    examples: { type: 'array', items: { type: 'object', required: ['dir', 'scala_passed', 'haskell_passed', 'mutation_detected', 'equivalent', 'issues'],
+      properties: { dir: { type: 'string' }, scala_passed: { type: 'boolean' }, haskell_passed: { type: 'boolean' }, mutation_detected: { type: 'boolean' }, equivalent: { type: 'boolean' }, issues: { type: 'array', items: { type: 'string' } } } } },
+    adversarial_findings: { type: 'array', items: { type: 'string' } },
+    report_file: { type: 'string' },
+  },
+}
+const DIAGRAM_SCHEMA = { type: 'object', required: ['files', 'notes'], properties: { files: { type: 'array', items: { type: 'string' } }, notes: { type: 'string' } } }
+
+const common = `Read ${BRIEF} first; it has the repo layout, toolchain commands, and constraints. Also read ${REPO}/.claude/skills/refactoring-entry/LESSONS.md: it lists what went wrong on previous entries. Work in the repo at ${REPO} (branch refactoring/${A.slug}). Do not commit.`
+
+// ---------------------------------------------------------------- Track A: research → verify citations → fix-up
+const trackA = async () => {
+  const research = await agent(`${common}
+
+You are the RESEARCH agent for catalogue entry ${A.number} of ${A.total}: "${A.name}", read as a Constructive/functional-programming refactoring, always presented WITH ITS DUAL (the inverse move: the two directions are one equation).
+Write ${SCRATCH}/research.md — the prose for the web page at /refactorings/${A.slug}/ — with these exact H2 headings, in this exact order; the first section is always Motivation. Match the reference page ${REPO}/pages/refactorings/extract-method.md in tone and depth (read it first):
+
+## Motivation
+The FIRST section, before any mechanics. Why reach for either direction, two short paragraphs: the smells that drive the move (duplication, long methods, ...) and the smells that drive its inverse (speculative generality, coupling through a seam's implementation rather than its contract, ...). The reader should know when to use the move before how to perform it.
+
+## The move
+The refactoring as the OO / imperative world catalogues it (Fowler, Kerievsky, Opdyke, the IDE menu, GoF where relevant): mechanics, preconditions, why they are needed there.
+
+## The functional reading
+What the move IS in a referentially transparent, typed language; which transformation systems and papers it is an instance of; how tools (HaRe, compilers, Scala refactoring library) perform it or its inverse. Explain what the constructive criteria (referential transparency, totality, termination) buy: the OO precondition becomes an equation or a type.
+
+## To and from
+The two directions as a pair. State the equation or the isomorphism. Say what each direction is *for*.
+
+## Pitfalls
+Concrete caveats, each one sentence + why: effects and evaluation order; sharing and evaluation count (Scala def/val, Haskell let/CAF, full laziness); strictness and bottom; exceptions and non-termination; name capture or type-inference changes; anything specific to this move.
+
+## Verification
+How the property-based test states the equivalence (forAll x. before x == after x), hedgehog both sides, and one paragraph on mutation-checking the spec.
+
+## References
+A numbered list. EVERY reference must be real. Use WebSearch/WebFetch to confirm title, authors, year, venue, and a working URL (DOI, ACM DL, author's page, or arXiv) for each one BEFORE including it. If you cannot verify an item, leave it out. Prefer primary sources. Aim for 10–14 references. Anchors to start from (verify them too):
+${SEEDS}
+Always include: Fowler (Refactoring, 1999 and/or 2018), Claessen & Hughes QuickCheck ICFP 2000, hedgehog (GitHub), and Thompson's "Refactoring functional programs" (AFP 2004, LNCS 3622) or HaRe where the move exists there.
+Cite in-text as [[n](#ref-n)], a link to the reference at the bottom of the page (sample the extract-method page source for the exact markup the reference list uses — raw <li id="ref-N"> items inside a plain <ol>, hand-rendered inline HTML). Prose: tight, editorial, 900–1500 words, sentences not bullets (the caveats section may use a short list). Claims about what a tool or paper does must be modest and literally supported by it. Do not write code. No Liquid-looking sequences ({{ or {%).
+
+Return the file path, the references array (id = the [n] number, plus title/authors/year/venue/url/claim), and a 3-sentence summary.`,
+    { label: `research:${A.slug}`, phase: 'Research', schema: RESEARCH_SCHEMA, effort: 'high' })
+  if (!research) return { research: null }
+  log(`research done: ${research.references.length} references`)
+
+  const verdicts = (await parallel(research.references.map(r => () =>
+    agent(`You are a citation SKEPTIC. Try to REFUTE this reference; default to ok=false if you cannot confirm it.
+Reference [${r.id}]: "${r.title}" — ${r.authors} (${r.year}), ${r.venue}. URL: ${r.url}
+Claim the text attributes to it: ${r.claim}
+
+Use WebFetch on the URL (and WebSearch if needed) and check: (1) the URL resolves and is about this work; (2) title, authors, year, venue are correct (small formatting differences are fine; wrong year/venue/author list is not); (3) the attributed claim is something this work actually says or does — an overstatement ("spends most of its effort", "proves", "always") counts as a failure. If the URL is dead but the work exists, find a working URL and return it as fixed_url. If a detail is wrong but the work exists, return the corrected citation line as fixed_citation. Return ok=true only when all three checks pass (possibly after your fix). Put what you checked in note (1–3 sentences).`,
+      { label: `cite:${r.id}`, phase: 'Citations', schema: CITE_SCHEMA })
+  ))).filter(Boolean)
+
+  const bad = verdicts.filter(v => !v.ok)
+  const fixes = verdicts.filter(v => v.ok && (v.fixed_url || v.fixed_citation))
+  log(`citations: ${verdicts.length - bad.length}/${verdicts.length} confirmed, ${bad.length} refuted, ${fixes.length} corrected`)
+
+  let fixup = 'no fix-up needed'
+  if (bad.length || fixes.length) {
+    fixup = await agent(`${common}
+Edit ${SCRATCH}/research.md in place. Independent skeptics checked every reference. Apply these results exactly:
+
+REFUTED (remove the reference, or replace it with a verified alternative you confirm yourself via WebFetch; rewrite any sentence that leaned on it so the text stays true and the numbering stays contiguous; if only the claim was overstated, tone the sentence down to what the source supports and keep the reference):
+${bad.map(v => `- [${v.id}] ${v.note}`).join('\n') || '- none'}
+
+CORRECTIONS (apply the corrected URL/citation line):
+${fixes.map(v => `- [${v.id}] ${v.fixed_citation || ''} ${v.fixed_url ? 'URL: ' + v.fixed_url : ''} — ${v.note}`).join('\n') || '- none'}
+
+Keep the section headings and length. Return a 2–3 sentence description of what changed and the final reference count.`,
+      { label: 'research:fixup', phase: 'Citations' })
+  }
+  return { research, verdicts, fixup }
+}
+
+// ---------------------------------------------------------------- Track B: examples → verify (loop) → diagrams
+const trackB = async () => {
+  const buildPrompt = `${common}
+
+You are the EXAMPLES agent. Build THREE examples of "${A.name}" as a functional refactoring, each in BOTH Scala 3 and Haskell, under ${EX}/NN-<ex>/ exactly as the brief's code layout describes (Before/After/Spec × .scala/.hs). Copy ${REPO}/pages/refactorings/extract-method/run.sh into ${EX}/run.sh unchanged. Suggested set — adjust if you find a better trio, but keep the progression simple → closes over context/effects → recursion or laziness matters:
+${EXAMPLE_IDEAS}
+Rules:
+- Before and After expose the SAME entry point (same name, same signature) so Spec can compare them; After differs from Before ONLY by the refactoring. Keep every file short and idiomatic (Scala 3 syntax, braces-free is fine; Haskell 2010 + common extensions only). Lines ≤ 72 characters. The Scala and Haskell Befores must have the same shape.
+- Spec generates meaningful inputs with hedgehog, designed around the program's boundaries (see the Generators section of the brief), and asserts before == after; add a second property per example when there is a natural one.
+- Scala Spec must be runnable with: scala-cli run ${EX}/NN-ex --main-class spec   (exit 1 on failure). Haskell Spec with the docker command in the brief.
+- RUN every spec in both languages yourself and only report scala_ok/haskell_ok=true when you saw it pass. Then run sh ${EX}/run.sh once from the repo root and confirm it ends with "all properties passed". Paste the last lines of output per example in output_tail.
+- Mutation-check your own specs once before returning: break After in a copy under ${SCRATCH}/mut/, confirm each property fails, restore. The reviewer will do this again with different mutants.
+- Do not create files outside ${EX}/ and ${SCRATCH}/. Leave no build artefacts outside .scala-build/ (gitignored).
+Return the examples array and notes (design choices, anything the page text should mention).`
+
+  let examples = await agent(buildPrompt, { label: 'examples:build', phase: 'Examples', schema: EXAMPLES_SCHEMA, effort: 'high' })
+  if (!examples) return { examples: null }
+  log(`examples built: ${examples.examples.map(e => e.dir).join(', ')}`)
+
+  const reviewPrompt = (round) => `${common}
+
+You are the REVIEWER. Independently confirm that each example under ${EX}/NN-*/ is a genuine equivalence, using the property-based tests, and try hard to break it. Round ${round}.
+Steps, all mandatory:
+1. Run sh ${EX}/run.sh from the repo root. Record per-example pass/fail for Scala and Haskell.
+2. Mutation check of each Spec, both languages: make a small semantic change to After (off-by-one, dropped case, swapped operands, boundary < vs <=) in a COPY (cp -r the example dir into ${SCRATCH}/mut/NN-ex, edit the copy, run the copy's spec with the same commands, paths adjusted). The property MUST fail on the mutant, reliably (run flaky catches 5 times); if it survives, the generator or property is too weak — report the exact generator change and test count that fixes it, measured. Never leave a mutation in the real files (git -C ${REPO} status --short pages/refactorings).
+3. Adversarial probes (throwaway specs in ${SCRATCH}/mut/, not in the repo): stronger generators (empty, negative, Int boundaries, deep ADTs); in Haskell, laziness/strictness — does After force something Before did not (undefined in lazily-unused positions, seq)? in Scala, evaluation count — does the refactoring change how many times something is evaluated (def vs val, by-name)? Totality: any partial function / non-exhaustive match introduced?
+4. Read Before vs After in each language: is the refactoring the ONLY difference? Same entry-point signature? Are the Scala and Haskell Befores parallel? Short and idiomatic enough for a public page? Lines ≤ 72 chars? Any {{ or {% sequences (forbidden)? Any comment that overclaims (e.g. "never throws" where Int arithmetic can)?
+Write a report to ${SCRATCH}/review-round${round}.md with a mutation table and a probe summary (the PR description quotes them). Return passed=true only if every example passes in both languages, every mutant was caught reliably, and no adversarial probe found a semantic difference. List concrete, actionable issues per example (file + what to change) — the examples agent will act on them verbatim.`
+
+  let verdict = null
+  for (let round = 1; round <= 3; round++) {
+    verdict = await agent(reviewPrompt(round), { label: `verify:round${round}`, phase: 'Verify', schema: VERIFY_SCHEMA, effort: 'high' })
+    if (!verdict) break
+    log(`verify round ${round}: ${verdict.passed ? 'PASSED' : 'issues: ' + verdict.examples.flatMap(e => e.issues).length}`)
+    if (verdict.passed) break
+    examples = await agent(`${common}
+
+You are the EXAMPLES agent again. The reviewer found problems in round ${round} (report: ${verdict.report_file}). Fix them in ${EX}/, keeping the same layout and rules as before. Issues:
+${verdict.examples.map(e => `- ${e.dir}: ${e.issues.join(' | ') || 'ok'}`).join('\n')}
+Adversarial findings: ${verdict.adversarial_findings.join(' | ') || 'none'}
+Re-run every spec in both languages and sh ${EX}/run.sh; re-run the reviewer's mutants against your fix; report only what you saw pass.`,
+      { label: `examples:fix${round}`, phase: 'Examples', schema: EXAMPLES_SCHEMA, effort: 'high' })
+    if (!examples) break
+  }
+
+  let diagrams = null
+  if (verdict && verdict.passed) {
+    diagrams = await agent(`${common}
+
+You are the DIAGRAM agent. Produce small inline-SVG diagrams for the page /refactorings/${A.slug}/, saved under ${EX}/. Read ${REPO}/pages/refactorings/extract-method/diagrams/koan.svg and one of its NN-*/diagram.svg first and match their visual language exactly (same stroke widths, fonts, arrow style, dashed region convention).
+- diagrams/koan.svg — the "to and from" pair for this refactoring: left = before-shape, right = after-shape, top arrow labelled with the move pointing right, bottom arrow labelled with the inverse pointing left. Use the terms from ${SCRATCH}/research.md's "To and from" section.
+- NN-<ex>/diagram.svg for each example directory present (read Before/After in that dir first): left = Before with the affected region drawn as a dashed inner rectangle; right = After with the new structure and the relationship (call, instance, parameter) named on the arrow. Use the real names from the code.
+Rules: viewBox-based, no fixed width/height; all strokes and text use currentColor so it works in light and dark themes; fills only rgba with low alpha or none; font-family: inherit; font-size 12–14 viewBox units; <title> for accessibility; role="img"; no external resources, no scripts, no site CSS classes; each file under 6 KB; NO {{ or {% sequences. Render-check each SVG with the chrome-devtools MCP tools (ToolSearch for mcp__chrome-devtools__new_page / take_screenshot; file:// URLs work) at 1000px and 360px wide and fix overlaps or clipped text. Return the list of files written and notes.`,
+      { label: 'diagrams', phase: 'Diagrams', schema: DIAGRAM_SCHEMA })
+  }
+  return { examples, verdict, diagrams }
+}
+
+const [a, b] = await parallel([trackA, trackB])
+return { research: a, examples: b }
diff --git a/.gitignore b/.gitignore
index 00108e1..51dfb96 100644
--- a/.gitignore
+++ b/.gitignore
@@ -64,3 +64,10 @@ typings/
 /Gemfile.lock
 /.jekyll-metadata
 .sass-cache/
+
+# Refactoring examples: scala-cli and GHC build output
+.scala-build/
+.bsp/
+dist-newstyle/
+*.hi
+*.o
diff --git a/_config.yml b/_config.yml
index e87b679..12eb19d 100644
--- a/_config.yml
+++ b/_config.yml
@@ -37,3 +37,8 @@ katex: true
 color_theme: auto
 remote_theme: sylhare/Type-on-Strap
 plugins: [jekyll-paginate, jekyll-seo-tag, jekyll-feed, jekyll-remote-theme]
+
+# Refactoring example sources are pulled into their page with
+# include_relative; do not also publish them as static files.
+exclude:
+  - pages/refactorings/extract-method/
diff --git a/_data/refactorings.yml b/_data/refactorings.yml
new file mode 100644
index 0000000..264354c
--- /dev/null
+++ b/_data/refactorings.yml
@@ -0,0 +1,47 @@
+# Constructive Programming refactorings — the catalogue at /refactorings/.
+# An item with a `slug` has a page at /refactorings/<slug>/; items without
+# one are listed unlinked until their page is written.
+
+- group: "Refactorings"
+  items:
+    - { name: "Extract / Inline method", slug: extract-method }
+    - { name: "Replace mutable fields with lenses" }
+    - { name: "Replace global state with parameter" }
+    - { name: "Introduce ReaderT (Kleisli)" }
+    - { name: "Replace loop with fold" }
+    - { name: "Replace recursion with fold" }
+    - { name: "Replace inheritance with natural transformation" }
+    - { name: "Replace exception with extended response type" }
+    - { name: "Replace null with optional" }
+    - { name: "Replace optional fields with sum types" }
+    - { name: "Replace sum types with optional fields" }
+    - { name: "Replace parameter with reduced type" }
+    - { name: "Replace mutable variable with recursion" }
+    - { name: "Replace similar methods with generic cousin" }
+    - { name: "Extract constant" }
+    - { name: "Merge into module" }
+    - { name: "Extract generic algebra" }
+    - { name: "Wrap side effect" }
+    - { name: "Pull out effect" }
+    - { name: "Lazy lists to eager arrows" }
+    - { name: "Replace unit tests with property-based test" }
+
+- group: "With higher-kinded types"
+  items:
+    - { name: "Generalize over input constraint" }
+    - { name: "Isolate business key via data parametrization" }
+    - { name: "Remove recursion from GADT" }
+    - { name: "Replace visitor with type class" }
+    - { name: "Replace concrete classes with final tagless interpretation" }
+    - { name: "Replace final tagless with free monad" }
+    - { name: "Replace free monad with final tagless encoding" }
+    - { name: "Replace strategy with tagless final" }
+    - { name: "Replace subtypes with type class instances" }
+    - { name: "Replace pattern matching with type class dispatch" }
+    - { name: "Introduce higher-kinded constraint" }
+
+- group: "With dependent types"
+  items:
+    - { name: "Introduce parameter-value-dependent constraint" }
+    - { name: "Introduce (path-)dependent type" }
+    - { name: "Replace (path-)dependent type with type class constraint" }
diff --git a/_posts/2019-10-18-Refactorings.md b/_posts/2019-10-18-Refactorings.md
deleted file mode 100644
index 9b5629e..0000000
--- a/_posts/2019-10-18-Refactorings.md
+++ /dev/null
@@ -1,46 +0,0 @@
----
-layout: post
-title: Refactorings
-tags: [refactoring, tools]
----
-
-# Refactorings
-
-1. Extract method.
-2. Replace mutable fields with lenses.
-3. Replace global state with parameter.
-4. Introduce ReaderT (Kleisli). 
-5. Replace loop with fold.
-6. Replace recursion with fold.
-7. Replace inheritance with natural transformation.
-8. Replace exception with extended response type.
-9. Replace null with optional.
-10. Replace optional fields with sum types. 
-11. Replace sum types with optional fields. 
-12. Replace parameter with reduced type.
-13. Replace mutable variable with recursion.
-14. Replace similar methods with generic cousin.
-15. Extract constant.
-16. Merge into module.
-17. Extract generic algebra.
-18. Wrap side effect.
-19. Pull out effect.
-
-## With higher kinded types:
-
-1. Generalize over input constraint. 
-2. Isolate business key via data parametrization. 
-3. Remove Recursion from GADT. 
-4. Replace visitor with type class. 
-5. Replace concrete classes with final tagless interpretation. 
-6. Replace final tagless with free monad. 
-7. Replace free monad with final tagless encoding. 
-8. Replace strategy with tagless final. 
-9. Replace subtypes with type class instances. 
-10. Replace pattern matching with type class dispatch. 
-
-## With dependent types :
-
-1. Introduce parameter value dependent constraint.
-2. Introduce (path) Dependent type.
-3. Replace (path) Dependent type with type class constraint. 
diff --git a/assets/css/main.scss b/assets/css/main.scss
index e2a3c42..c8ec03a 100644
--- a/assets/css/main.scss
+++ b/assets/css/main.scss
@@ -773,3 +773,47 @@ html[data-theme="dark"] .site-footer .footer-icons a:hover { color: $cp-accent-d
    its tokens win over the generic card/button rules above.
    ============================================================ */
 @import 'home';
+
+/* ============================================================
+   Refactoring catalogue — /refactorings/ and its entries.
+   ============================================================ */
+.refactoring-list li { margin-bottom: 0.2rem; }
+.refactoring-pending { opacity: 0.55; }
+
+/* Entry pages: Scala and Haskell side by side on wide viewports,
+   stacked below. Each pane scrolls on its own so the page never
+   scrolls horizontally. */
+.rf-pair {
+  display: grid;
+  grid-template-columns: 1fr;
+  gap: 1rem;
+  margin: 1rem 0 2rem;
+}
+@media (min-width: 1000px) {
+  /* Bleed past the prose measure so two 80-column panes fit side by side. */
+  .rf-pair {
+    grid-template-columns: 1fr 1fr;
+    width: min(100vw - 3rem, 1360px);
+    margin-left: calc(50% - min(50vw - 1.5rem, 680px));
+  }
+}
+.rf-pair > div { min-width: 0; }
+.rf-pair pre, .rf-pair code { font-size: 0.78rem; }
+.rf-pair h4 {
+  font-family: $cp-mono;
+  font-size: 0.8rem;
+  letter-spacing: 0.04em;
+  text-transform: uppercase;
+  opacity: 0.7;
+  margin: 0 0 0.4rem;
+}
+.rf-pair pre { overflow-x: auto; margin: 0; }
+.rf-pair .highlight { margin: 0; }
+
+.rf-figure { margin: 2rem 0; }
+.rf-figure svg { width: 100%; height: auto; display: block; }
+.rf-figure figcaption { font-size: 0.9rem; opacity: 0.75; margin-top: 0.5rem; }
+.rf-crumb { font-size: 0.9rem; opacity: 0.75; margin-bottom: 1.5rem; }
+.rf-spec { margin: 1rem 0 2rem; }
+.rf-spec summary { cursor: pointer; font-size: 0.95rem; }
+.rf-spec[open] summary { margin-bottom: 0.75rem; }
diff --git a/pages/refactorings.md b/pages/refactorings.md
new file mode 100644
index 0000000..8fd6053
--- /dev/null
+++ b/pages/refactorings.md
@@ -0,0 +1,35 @@
+---
+layout: page
+title: Refactorings
+subtitle: The Constructive Programming refactoring catalogue
+permalink: /refactorings/
+tags: refactorings
+---
+
+Object-oriented developers have a shared vocabulary for reshaping code
+without changing what it does — Fowler's catalogue, Opdyke's thesis, the
+*Refactoring* menu in every IDE — as well as a history of doing so
+informally before then. This is the same idea seen
+through the functional-programming imagination: each move takes a program
+from one
+structure to an equivalent one, and in a referentially transparent
+setting *equivalent* is something you can state and check.
+
+Every entry that has a page shows the refactoring in **Scala 3** and in
+**Haskell**, in both directions (the move and its inverse), with the
+papers and study material behind it, a diagram of the structural change,
+and a property-based test — [Hedgehog](https://github.com/hedgehogqa/scala-hedgehog)
+in Scala and [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog) in Haskell —
+that exercises the *before* and *after* on generated inputs and demands
+the same answer. Entries without a link are queued; they will be filled
+in the order listed.
+
+{% for group in site.data.refactorings %}
+## {{ group.group }}
+
+<ol class="refactoring-list">
+{% for item in group.items -%}
+  <li>{% if item.slug %}<a href="{{ '/refactorings/' | append: item.slug | append: '/' | relative_url }}">{{ item.name }}</a>{% else %}<span class="refactoring-pending">{{ item.name }}</span>{% endif %}</li>
+{% endfor -%}
+</ol>
+{% endfor %}
diff --git a/pages/refactorings/extract-method.md b/pages/refactorings/extract-method.md
new file mode 100644
index 0000000..63be413
--- /dev/null
+++ b/pages/refactorings/extract-method.md
@@ -0,0 +1,413 @@
+---
+layout: page
+title: Extract / Inline Method
+subtitle: "Extract / Inline method: name a sub-expression, and its free variables become the parameters — inline a call, and its arguments flow back into the body"
+permalink: /refactorings/extract-method/
+tags: [refactorings, extract-method]
+hide: true   # entry pages are reached from the catalogue, not the top-right nav
+---
+
+<p class="rf-crumb"><a href="{{ '/refactorings/' | relative_url }}">← The refactoring catalogue</a> · 1 of 35</p>
+
+Extract / Inline Method is the pair everyone learns first. Extract: find
+a region of a method body that does one nameable thing, move it into a
+new method, and replace the region with a call. Inline: take a call and
+replace it with the body of the method it names. Fowler's 1999 catalogue
+gave Extract that name [[1](#ref-1)]; the second edition renamed it Extract
+Function, lists Inline Function as its inverse, and rewrote the mechanics
+for a language without classes [[2](#ref-2)]. The lineage is older. Griswold's 1991
+thesis treated
+restructuring as meaning-preserving manipulation of a program dependence
+graph, with a tool holding the semantics fixed while the programmer moved
+code about [[4](#ref-4)]. Opdyke's 1992 thesis gave the first full treatment of
+"refactoring" for the object-oriented setting, and stated each operation
+as a transformation with explicit preconditions under which behaviour is
+preserved [[3](#ref-3)].
+
+## Motivation
+
+The two directions answer different [code smells](https://en.wikipedia.org/wiki/Code_smell), and the direction you choose
+records a judgement about the code. Extract when the same shape of work
+recurs in more than one place and the duplication would otherwise drift
+out of sync, each copy fixed separately; or when a method has grown so
+long that its single responsibility is no longer visible. Naming the
+region gives the recurring or the long shape a signature and a boundary
+of its own — it can be reused, tested and varied, and the reader no
+longer holds the whole method in their head.
+
+Inline when the indirection costs more than it names. A method that
+exists only because some future boundary might need it is speculative
+generality: abstraction tax paid today for flexibility nobody uses. And
+a seam whose callers are coupled through its implementation rather than
+its contract hides nothing — the name adds a hop, not meaning. Inlining
+removes the hop and lets the body breathe into the caller, where the
+constants and structure the name kept apart become visible again.
+
+Both languages here let a method nest inside the method that uses it, and
+that adds a third, finer judgement: where exactly the boundary falls. When
+you extract into a nested method, the values the region still sees from the
+enclosing scope simply stay in scope — they are *captured*, not passed —
+and only the values it needs from further out become the actual parameters.
+Choosing the scope of the extraction is therefore a judgement about which
+values should remain accessible and which should be made explicit, and the
+same region can be rendered with all of its dependencies in scope, or with
+some, or with none. The worst of the three looks like the same program with
+an extra name; the best gives the step function a boundary as sharp as a
+top-level one.
+
+## The move
+
+Fowler's mechanics are short: create a method named for what the region
+does, copy the region into it, pass the locals the region reads as
+parameters, return the locals it writes or refuse, replace the region with
+the call, test [[1](#ref-1)], [[2](#ref-2)]. "Refuse" is where the preconditions live. In an
+imperative language a region of statements is not a value; it is a
+sequence of effects on a mutable environment. The extracted method must
+see the same environment the region saw, hand back every change the rest
+of the method depends on, and run exactly as often, in the same position,
+as the region ran. A region that assigns two locals, or whose reads are
+interleaved with writes to the same fields elsewhere, cannot be lifted
+without changing the program. Fowler's advice to reduce temps first pushes
+the code toward the case where extraction is safe; Opdyke's precondition
+list makes the same demand formally [[3](#ref-3)]. Every automated refactoring tool
+since, including Stocker's Scala refactoring library behind the Scala IDE
+[[15](#ref-15)], must perform exactly this analysis.
+
+## To and from
+
+<figure class="rf-figure">
+{% include_relative extract-method/diagrams/koan.svg %}
+<figcaption>The koan. One equation, read in two directions: extract
+(define and fold; lambda-lift, or simply nest the definition) to the
+right, inline (unfold and β-reduce; denest) to the left. The free
+variables of the region <em>e</em> become the parameters of a top-level
+definition — nested, they stay in the enclosing scope instead, and only
+what lies further out is passed.</figcaption>
+</figure>
+
+The catalogue lists each refactoring in both directions because the two
+moves are one equation read left to right and right to left. For a
+definition *f* with parameters *x₁ … xₙ* and body *e*, *f a₁ … aₙ* equals
+*e* with each *xᵢ* replaced by *aᵢ*, provided no *aᵢ* is captured by a
+binder inside *e*. Read from application to body it is Inline: unfold,
+substitute, and if the arguments were variables the result is what stood
+there before. Read from body to application it is Extract: choose the
+region *e*, take its free variables as the *xᵢ*, and fold.
+
+The directions serve different ends. Extract is for naming, so a reader
+sees what the region means rather than how; for reuse, so a second
+occurrence becomes a second call; and for generalisation, because once the
+free variables are parameters any of them can be varied and a specific
+expression becomes a function over a family. Inline is for
+specialisation, because unfolding at a call site with known arguments
+exposes constants and structure that further rewrites can act on, and for
+removing indirection that no longer earns its name. Burstall and
+Darlington's system gets almost all of its power from alternating the
+two: unfold to expose a pattern, apply a law, fold to recover a recursion
+with a better shape [[5](#ref-5)]. A compiler's simplifier works the unfolding half
+at scale [[9](#ref-9)]. The programmer works at a larger grain with a different
+objective, but the moves are the same moves.
+
+## Three examples
+
+Each example is the same program twice, `Before` and `After`, in Scala 3
+and in Haskell. The entry point keeps its name and its type, the
+extraction is the only difference, and a hedgehog property generates
+inputs and demands that both versions agree on every one of them. The
+sources below are included verbatim from the files the tests run against.
+
+### 1 · Order total: the textbook move
+
+A subtotal, a percentage discount, a percentage tax. The region `amount ×
+pct / 100` appears twice with different free variables, so it becomes
+`percent(pct, amount)`; the line sum has no free variables beyond the
+list, so it becomes `subtotal(items)`. Nothing in the region closes over
+anything the new functions cannot be handed as an argument.
+
+<figure class="rf-figure">
+{% include_relative extract-method/01-order-total/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/01-order-total/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/01-order-total/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/01-order-total/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/01-order-total/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+Note what did *not* change: `net` is still bound once, so `subtotal` is
+still computed once. Extracting a function and then calling it twice
+would have been a second, different refactoring.
+
+<details class="rf-spec">
+<summary>The property: <code>Before.total == After.total</code> on generated orders</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/01-order-total/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/01-order-total/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+### 2 · Running balance: the region closes over locals
+
+The fold's step function reads `limit` and `fee`, which are parameters of
+`settle`. A top-level extraction would have to make those free variables
+leading parameters — Johnsson's lambda lifting [[6](#ref-6)], and HaRe's *generalise
+definition* [[10](#ref-10)]. But both languages also let the definition stay where it
+is used: `step` nests inside `settle`, `limit` and `fee` remain in scope
+and are captured, and only `balance` and `tx` — the values the fold
+supplies — become the parameters. This is the scope judgement from the
+Motivation section: the same region, extracted with its dependencies kept
+in scope instead of made explicit, earns a boundary of its own without
+giving its caller a new signature.
+
+<figure class="rf-figure">
+{% include_relative extract-method/02-running-balance/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/02-running-balance/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/02-running-balance/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/02-running-balance/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/02-running-balance/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+Nesting keeps `step` private: callers of `settle` can observe only that
+the closing balance agrees with the unrefactored version — exactly what
+the single property checks. The inverse picture is Danvy and Schultz's
+lambda dropping [[7](#ref-7)], restoring block structure by dropping parameters
+that are invariant across a call graph back into scope.
+
+<details class="rf-spec">
+<summary>The property: <code>Before.settle == After.settle</code> on generated transaction runs</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/02-running-balance/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/02-running-balance/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+### 3 · Expression evaluator: extraction inside a recursive match
+
+Three cases of a recursive evaluator share a shape: evaluate the left
+operand, then the right, then combine, with division by zero yielding no
+value rather than an exception. The shape becomes `binary`, parameterised
+by the combining operation. The one design decision is that `binary`
+takes the operands *unevaluated*: hand it `eval(l)` and `eval(r)` instead
+and Scala would evaluate the right operand even when the left one has no
+value, which `Before` never did. In Haskell the same choice keeps the
+short-circuit exact under laziness, and the second property checks it by
+putting `undefined` in the right operand. One partiality survives on both
+sides: Haskell's `div` still overflows at `minBound` divided by `-1`. The
+refactoring preserves that; it does not fix it, and the property confirms
+that both versions throw on the same input.
+
+<figure class="rf-figure">
+{% include_relative extract-method/03-expression-eval/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/03-expression-eval/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/03-expression-eval/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/03-expression-eval/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/03-expression-eval/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+<details class="rf-spec">
+<summary>The property: <code>Before.eval == After.eval</code> on generated trees, and the short-circuit survives</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative extract-method/03-expression-eval/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative extract-method/03-expression-eval/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+## Pitfalls
+
+The equation has hypotheses, and each is one of the constructive
+criteria. Where a hypothesis fails, extraction changes the program.
+In a language with referential transparency the OO precondition does not
+become easier to satisfy; it disappears, and the move becomes an equation.
+The structures that make that true are gathered in the footnote at the end
+of this section.
+
+- **Side effects and evaluation order.** If the region performs effects,
+  moving it into a definition can change when and how often they happen.
+  This is the OO precondition, and the only one imperative languages need
+  because it subsumes the rest. In Scala a `def` is re-evaluated at each
+  call and a `val` once, so extracting an effectful expression into a
+  `def` can multiply effects, and into a `val` can move them to
+  initialisation.
+- **Sharing and evaluation count.** In a pure language the value is the
+  same but the work may not be. A Scala `def` recomputes; a `val` shares.
+  In Haskell a `let`-bound expression is evaluated at most once per
+  binding, a top-level constant applicative form is shared for the
+  program's lifetime, and a function body is recomputed per call unless
+  full laziness floats it out [[8](#ref-8)]. Extraction can change space and time,
+  including turning a bounded computation into a leak, without changing
+  the result.
+- **Strictness.** A definition that pattern-matches on a parameter forces
+  it when applied, even if the original expression only used it in a
+  branch not taken. Extraction can introduce a force and inlining remove
+  one; where the argument is bottom the two programs differ. Totality, no
+  `undefined` and no partial functions, is exactly the condition under
+  which this cannot arise. Example 3 is built around this.
+- **Exceptions and non-termination.** An expression that throws or
+  diverges is a value only in a language that models those outcomes as
+  values. If the region can throw and the call site evaluates it in a
+  different order, the exception observed changes; if it can diverge, the
+  strictness argument applies. Termination removes the second case, total
+  error handling the first.
+- **Name capture.** Substituting the body for the call, or lifting the
+  region past a binder, must not let a free variable of the region be
+  captured by an inner binding of the same name. Tools rename; by hand
+  this is the commonest way to make Inline wrong. A type checker catches
+  most captures, since a captured variable usually has the wrong type,
+  but not all.
+
+In each case the fix is the same: restore the hypothesis, by making the
+region pure, total and terminating and by renaming, or admit that this is
+not a refactoring and test it as a change.
+
+<details class="rf-spec">
+<summary>The functional reading</summary>
+<div markdown="1">
+
+In a referentially transparent language the region is an expression, and
+an expression depends only on its free variables. Extracting it means
+naming it: write a definition whose parameters are the free variables of
+the region and whose body is the region, then replace the region with an
+application of the new name to those variables. There is no environment
+to rebuild because there is no environment; the free variables are the
+whole of what the expression could see, and the type checker tells you
+what they are.
+
+This is not a new idea dressed up. It is the abstraction step of Burstall
+and Darlington's 1977 fold/unfold system, where a program is a set of
+equations and the permitted moves are to define a new equation, to unfold
+a call by replacing it with its right-hand side, and to fold a
+sub-expression back into a call wherever it matches one [[5](#ref-5)]. Extract is
+definition followed by fold; Inline is unfold. Johnsson's lambda lifting,
+which turns nested local functions into top-level equations by adding
+their free variables as parameters, is extraction pushed to the whole
+program [[6](#ref-6)]; Danvy and Schultz's lambda dropping is the inverse, restoring
+block structure by dropping parameters that are invariant across a call
+graph back into scope [[7](#ref-7)]. Let-floating in GHC moves bindings inward or
+outward for sharing and allocation, relying on the same fact that a
+binding may be placed anywhere its free variables are in scope [[8](#ref-8)]. And
+GHC's inliner performs the inverse of extraction thousands of times a
+build, unfolding and beta-reducing wherever the result is smaller or
+faster; Peyton Jones and Marlow's account of it is, read from the other
+side, an account of when extraction costs nothing at runtime [[9](#ref-9)].
+
+The Haskell Refactorer, HaRe, offers the pair as tool operations:
+*introduce definition*, which names a selected sub-expression;
+*generalise definition*, which turns a sub-expression into a parameter;
+and *unfold*, which replaces a call with the body [[10](#ref-10)], [[11](#ref-11)]. Thompson's
+Advanced Functional Programming lecture notes set these out as equations
+between programs and discuss where the equations hold [[12](#ref-12)].
+
+That is the point. With referential transparency the OO precondition does
+not become easier to satisfy; it disappears, because the transformation is
+an instance of the language's own equational theory. Replacing an
+expression with a name bound to it is the beta rule read backwards.
+Extraction stops being something you hope preserved behaviour and becomes
+an equation you wrote down.
+
+</div>
+</details>
+
+## Verification
+
+Because extraction is an equation, its correctness is a property: for all
+inputs *x* in the domain of the entry point, `Before x == After x`. That is
+a one-line property in the sense Claessen and Hughes introduced with
+QuickCheck, where a generator produces inputs and the framework searches
+for a counterexample and shrinks it to a minimal one [[13](#ref-13)]. The catalogue
+states every entry this way, in Scala and in Haskell, with hedgehog on
+both sides [[14](#ref-14)]. Hedgehog is used because its shrinking is integrated
+into the generator, so a shrunk counterexample obeys the same invariants
+as a generated one and the minimal failing input it reports is a real
+input of the program, not an artefact of a separate shrinker.
+
+A property is only worth having if it can fail, so each spec above was
+mutation-checked: change `After` so it is no longer equivalent, by
+dropping a parameter, altering a boundary or reordering a match, confirm
+the property reports and shrinks a counterexample, then restore `After`.
+A property that does not fail under mutation is testing the generator,
+not the refactoring.
+
+To run everything on this page yourself, from a checkout of
+[the site repository](https://github.com/Constructive-Programming/website):
+
+```sh
+sh pages/refactorings/extract-method/run.sh
+```
+
+It needs [scala-cli](https://scala-cli.virtuslab.org/) and either GHC
+with hedgehog installed or Docker, and ends with `all properties passed`.
+
+## References
+
+<ol>
+<li id="ref-1">Martin Fowler, with contributions by Kent Beck, John Brant, William Opdyke and Don Roberts. <em>Refactoring: Improving the Design of Existing Code</em>. Addison-Wesley, 1999. <a href="https://martinfowler.com/books/refactoring.html">https://martinfowler.com/books/refactoring.html</a></li>
+<li id="ref-2">Martin Fowler. <em>Refactoring: Improving the Design of Existing Code</em>, second edition. Addison-Wesley, 2018. Catalogue entry &ldquo;Extract Function&rdquo; (formerly Extract Method; inverse of Inline Function). <a href="https://refactoring.com/catalog/extractFunction.html">https://refactoring.com/catalog/extractFunction.html</a></li>
+<li id="ref-3">William F. Opdyke. <em>Refactoring Object-Oriented Frameworks</em>. PhD thesis, University of Illinois at Urbana-Champaign, 1992 (Tech. Report UIUCDCS-R-92-1759). <a href="https://www.laputan.org/pub/papers/opdyke-thesis.pdf">https://www.laputan.org/pub/papers/opdyke-thesis.pdf</a></li>
+<li id="ref-4">William G. Griswold. <em>Program Restructuring as an Aid to Software Maintenance</em>. PhD thesis, University of Washington, 1991. Technical report 91-08-04. <a href="https://cseweb.ucsd.edu/~wgg/Abstracts/gristhesis.pdf">https://cseweb.ucsd.edu/~wgg/Abstracts/gristhesis.pdf</a></li>
+<li id="ref-5">R. M. Burstall and John Darlington. &ldquo;A Transformation System for Developing Recursive Programs&rdquo;. <em>Journal of the ACM</em> 24(1):44&ndash;67, 1977. <a href="https://doi.org/10.1145/321992.321996">https://doi.org/10.1145/321992.321996</a></li>
+<li id="ref-6">Thomas Johnsson. &ldquo;Lambda Lifting: Transforming Programs to Recursive Equations&rdquo;. In <em>Functional Programming Languages and Computer Architecture (FPCA 1985)</em>, LNCS 201, pp. 190&ndash;203. Springer, 1985. <a href="https://doi.org/10.1007/3-540-15975-4_37">https://doi.org/10.1007/3-540-15975-4_37</a></li>
+<li id="ref-7">Olivier Danvy and Ulrik P. Schultz. &ldquo;Lambda-dropping: transforming recursive equations into programs with block structure&rdquo;. <em>Theoretical Computer Science</em> 248(1&ndash;2):243&ndash;287, 2000. <a href="https://www.sciencedirect.com/science/article/pii/S0304397500000542">https://www.sciencedirect.com/science/article/pii/S0304397500000542</a></li>
+<li id="ref-8">Simon Peyton Jones, Will Partain and Andr&eacute; Santos. &ldquo;Let-floating: moving bindings to give faster programs&rdquo;. In <em>Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 1996)</em>, pp. 1&ndash;12. <a href="https://doi.org/10.1145/232627.232630">https://doi.org/10.1145/232627.232630</a></li>
+<li id="ref-9">Simon Peyton Jones and Simon Marlow. &ldquo;Secrets of the Glasgow Haskell Compiler inliner&rdquo;. <em>Journal of Functional Programming</em> 12(4&ndash;5):393&ndash;434, 2002. <a href="https://doi.org/10.1017/S0956796802004331">https://doi.org/10.1017/S0956796802004331</a></li>
+<li id="ref-10">Huiqing Li, Claus Reinke and Simon Thompson. &ldquo;Tool support for refactoring functional programs&rdquo;. In <em>Proceedings of the ACM SIGPLAN Workshop on Haskell (Haskell 2003)</em>, pp. 27&ndash;38. <a href="https://doi.org/10.1145/871895.871899">https://doi.org/10.1145/871895.871899</a></li>
+<li id="ref-11">Huiqing Li, Simon Thompson and Claus Reinke. &ldquo;The Haskell Refactorer, HaRe, and its API&rdquo;. <em>Electronic Notes in Theoretical Computer Science</em> 141(4):29&ndash;34, 2005 (LDTA 2005). <a href="https://doi.org/10.1016/j.entcs.2005.02.053">https://doi.org/10.1016/j.entcs.2005.02.053</a></li>
+<li id="ref-12">Simon Thompson. &ldquo;Refactoring Functional Programs&rdquo;. In <em>Advanced Functional Programming (AFP 2004), Revised Lectures</em>, LNCS 3622, pp. 331&ndash;357. Springer, 2005. <a href="https://doi.org/10.1007/11546382_9">https://doi.org/10.1007/11546382_9</a></li>
+<li id="ref-13">Koen Claessen and John Hughes. &ldquo;QuickCheck: a lightweight tool for random testing of Haskell programs&rdquo;. In <em>Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2000)</em>, pp. 268&ndash;279. <a href="https://doi.org/10.1145/351240.351266">https://doi.org/10.1145/351240.351266</a></li>
+<li id="ref-14">Jacob Stanley and contributors. <em>Hedgehog: release with confidence, state-of-the-art property testing</em>. <a href="https://github.com/hedgehogqa/haskell-hedgehog">https://github.com/hedgehogqa/haskell-hedgehog</a> and <a href="https://github.com/hedgehogqa/scala-hedgehog">https://github.com/hedgehogqa/scala-hedgehog</a></li>
+<li id="ref-15">Mirko Stocker. <em>Scala Refactoring</em>. Master&rsquo;s thesis, HSR Hochschule f&uuml;r Technik Rapperswil, 2010. <a href="https://eprints.ost.ch/id/eprint/286/">https://eprints.ost.ch/id/eprint/286/</a></li>
+</ol>
+
+
+
diff --git a/pages/refactorings/extract-method/01-order-total/After.hs b/pages/refactorings/extract-method/01-order-total/After.hs
new file mode 100644
index 0000000..348e02a
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/After.hs
@@ -0,0 +1,17 @@
+-- Total of an order: the lines summed, less a percentage discount, plus tax.
+module After where
+
+data Line  = Line  { unitPrice :: Int, quantity :: Int }
+data Order = Order { items :: [Line], discountPct :: Int, taxPct :: Int }
+
+total :: Order -> Int
+total o = discounted + percent (taxPct o) discounted
+  where
+    net        = subtotal (items o)
+    discounted = net - percent (discountPct o) net
+
+subtotal :: [Line] -> Int
+subtotal ls = sum [unitPrice l * quantity l | l <- ls]
+
+percent :: Int -> Int -> Int
+percent pct amount = amount * pct `div` 100
diff --git a/pages/refactorings/extract-method/01-order-total/After.scala b/pages/refactorings/extract-method/01-order-total/After.scala
new file mode 100644
index 0000000..9698a6c
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/After.scala
@@ -0,0 +1,15 @@
+// Total of an order: the lines summed, less a percentage discount, plus tax.
+object After:
+  case class Line(unitPrice: Int, quantity: Int)
+  case class Order(items: List[Line], discountPct: Int, taxPct: Int)
+
+  def total(o: Order): Int =
+    val net        = subtotal(o.items)
+    val discounted = net - percent(o.discountPct, net)
+    discounted + percent(o.taxPct, discounted)
+
+  def subtotal(items: List[Line]): Int =
+    items.map(l => l.unitPrice * l.quantity).sum
+
+  def percent(pct: Int, amount: Int): Int =
+    amount * pct / 100
diff --git a/pages/refactorings/extract-method/01-order-total/Before.hs b/pages/refactorings/extract-method/01-order-total/Before.hs
new file mode 100644
index 0000000..b20fa33
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/Before.hs
@@ -0,0 +1,11 @@
+-- Total of an order: the lines summed, less a percentage discount, plus tax.
+module Before where
+
+data Line  = Line  { unitPrice :: Int, quantity :: Int }
+data Order = Order { items :: [Line], discountPct :: Int, taxPct :: Int }
+
+total :: Order -> Int
+total o = discounted + discounted * taxPct o `div` 100
+  where
+    subtotal   = sum [unitPrice l * quantity l | l <- items o]
+    discounted = subtotal - subtotal * discountPct o `div` 100
diff --git a/pages/refactorings/extract-method/01-order-total/Before.scala b/pages/refactorings/extract-method/01-order-total/Before.scala
new file mode 100644
index 0000000..a510436
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/Before.scala
@@ -0,0 +1,9 @@
+// Total of an order: the lines summed, less a percentage discount, plus tax.
+object Before:
+  case class Line(unitPrice: Int, quantity: Int)
+  case class Order(items: List[Line], discountPct: Int, taxPct: Int)
+
+  def total(o: Order): Int =
+    val subtotal   = o.items.map(l => l.unitPrice * l.quantity).sum
+    val discounted = subtotal - subtotal * o.discountPct / 100
+    discounted + discounted * o.taxPct / 100
diff --git a/pages/refactorings/extract-method/01-order-total/Spec.hs b/pages/refactorings/extract-method/01-order-total/Spec.hs
new file mode 100644
index 0000000..a785835
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/Spec.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+-- Raw values, so the same input can be fed to both Before.Order and After.Order.
+genLine :: Gen (Int, Int)
+genLine = (,) <$> Gen.int (Range.linear (-100) 1000) <*> Gen.int (Range.linear 0 20)
+
+genOrder :: Gen ([(Int, Int)], Int, Int)
+genOrder = (,,) <$> Gen.list (Range.linear 0 10) genLine
+                <*> Gen.int (Range.linear 0 100)
+                <*> Gen.int (Range.linear 0 30)
+
+prop_total_agrees :: Property
+prop_total_agrees = property $ do
+  (items, d, t) <- forAll genOrder
+  Before.total (Before.Order (map (uncurry Before.Line) items) d t)
+    === After.total (After.Order (map (uncurry After.Line) items) d t)
+
+prop_plain_total_is_subtotal :: Property
+prop_plain_total_is_subtotal = property $ do
+  items <- forAll (Gen.list (Range.linear 0 10) genLine)
+  let ls = map (uncurry After.Line) items
+  After.total (After.Order ls 0 0) === After.subtotal ls
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("total: Before == After", prop_total_agrees)
+    , ("no discount, no tax: total == subtotal", prop_plain_total_is_subtotal)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/extract-method/01-order-total/Spec.scala b/pages/refactorings/extract-method/01-order-total/Spec.scala
new file mode 100644
index 0000000..70023e2
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/Spec.scala
@@ -0,0 +1,41 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("total: Before == After", totalAgrees),
+    property("no discount, no tax: total == subtotal", plainTotalIsSubtotal),
+  )
+
+  // Raw values, so the same input can be fed to both Before.Order and After.Order.
+  val genLine: Gen[(Int, Int)] =
+    for p <- Gen.int(Range.linear(-100, 1000)); q <- Gen.int(Range.linear(0, 20)) yield (p, q)
+  val genOrder: Gen[(List[(Int, Int)], Int, Int)] =
+    for
+      items <- genLine.list(Range.linear(0, 10))
+      d     <- Gen.int(Range.linear(0, 100))
+      t     <- Gen.int(Range.linear(0, 30))
+    yield (items, d, t)
+
+  def totalAgrees: Property =
+    for o <- genOrder.forAll
+    yield
+      val (items, d, t) = o
+      Before.total(Before.Order(items.map(Before.Line(_, _)), d, t))
+        ==== After.total(After.Order(items.map(After.Line(_, _)), d, t))
+
+  def plainTotalIsSubtotal: Property =
+    for items <- genLine.list(Range.linear(0, 10)).forAll
+    yield
+      val lines = items.map(After.Line(_, _))
+      After.total(After.Order(lines, 0, 0)) ==== After.subtotal(lines)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default), t.result, Seed.fromTime())
+    println(Test.renderReport("Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/extract-method/01-order-total/diagram.svg b/pages/refactorings/extract-method/01-order-total/diagram.svg
new file mode 100644
index 0000000..2b714c0
--- /dev/null
+++ b/pages/refactorings/extract-method/01-order-total/diagram.svg
@@ -0,0 +1,62 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 244" role="img" aria-labelledby="d1-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d1-title">Extracting subtotal and percent from total. Before: total(o) computes the line sum, the discount and the tax inline; the line sum and the two "amount times pct over 100" expressions are marked as regions. After: total(o) calls subtotal(items) with o.items, and percent(pct, amount) twice, with (o.discountPct, net) and (o.taxPct, discounted).</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="144" rx="4"/>
+    <rect x="428" y="36" width="336" height="90" rx="4"/>
+    <rect x="428" y="186" width="132" height="42" rx="4"/>
+    <rect x="580" y="186" width="184" height="42" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="46" y="81" width="340" height="18" rx="3"/>
+    <rect x="46" y="117" width="340" height="18" rx="3"/>
+    <rect x="46" y="153" width="340" height="18" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">total(o) =</text>
+    <text x="40" y="76">val subtotal =</text>
+    <text x="52" y="94">o.items.map(l =&gt; l.unitPrice * l.quantity).sum</text>
+    <text x="40" y="112">val discounted = subtotal -</text>
+    <text x="52" y="130">subtotal * o.discountPct / 100</text>
+    <text x="40" y="148">discounted +</text>
+    <text x="52" y="166">discounted * o.taxPct / 100</text>
+    <text x="440" y="58">total(o) =</text>
+    <text x="452" y="76">val net = subtotal(o.items)</text>
+    <text x="452" y="94">val discounted = net - percent(o.discountPct, net)</text>
+    <text x="452" y="112">discounted + percent(o.taxPct, discounted)</text>
+  </g>
+  <g fill="currentColor" font-size="13" font-weight="600">
+    <text x="440" y="212">subtotal(items)</text>
+    <text x="592" y="212">percent(pct, amount)</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="81" r="7.5"/>
+    <circle cx="386" cy="117" r="7.5"/>
+    <circle cx="386" cy="153" r="7.5"/>
+    <circle cx="428" cy="186" r="7.5"/>
+    <circle cx="580" cy="186" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="85">1</text>
+    <text x="386" y="121">2</text>
+    <text x="386" y="157">2</text>
+    <text x="428" y="190">1</text>
+    <text x="580" y="190">2</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M494 126 V178"/>
+    <path d="M672 126 V178"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M490.5 178 L494 186 L497.5 178 Z"/>
+    <path d="M668.5 178 L672 186 L675.5 178 Z"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="end">
+    <text x="486" y="160">o.items</text>
+    <text x="664" y="152">o.discountPct, net</text>
+    <text x="664" y="170">o.taxPct, discounted</text>
+  </g>
+</svg>
diff --git a/pages/refactorings/extract-method/02-running-balance/After.hs b/pages/refactorings/extract-method/02-running-balance/After.hs
new file mode 100644
index 0000000..4424449
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/After.hs
@@ -0,0 +1,13 @@
+-- Closing balance after a run of transactions; `step` is extracted from
+-- the fold lambda and stays nested, capturing `limit` and `fee`.
+module After where
+
+import Data.List (foldl')
+
+settle :: Int -> Int -> Int -> [Int] -> Int
+settle opening limit fee =
+  foldl' step opening
+  where
+    step balance tx =
+      let next = balance + tx
+      in if tx < 0 && next < negate limit then next - fee else next
diff --git a/pages/refactorings/extract-method/02-running-balance/After.scala b/pages/refactorings/extract-method/02-running-balance/After.scala
new file mode 100644
index 0000000..ceadbed
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/After.scala
@@ -0,0 +1,8 @@
+// Closing balance after a run of transactions; `step` is extracted from
+// the fold lambda and stays nested, capturing `limit` and `fee`.
+object After:
+  def settle(opening: Int, limit: Int, fee: Int, txs: List[Int]): Int =
+    def step(balance: Int, tx: Int): Int =
+      val next = balance + tx
+      if tx < 0 && next < -limit then next - fee else next
+    txs.foldLeft(opening)(step)
diff --git a/pages/refactorings/extract-method/02-running-balance/Before.hs b/pages/refactorings/extract-method/02-running-balance/Before.hs
new file mode 100644
index 0000000..2fb0bdf
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/Before.hs
@@ -0,0 +1,13 @@
+-- Closing balance after a run of transactions; a debit that leaves
+-- the account below its overdraft limit is charged a fee.
+module Before where
+
+import Data.List (foldl')
+
+settle :: Int -> Int -> Int -> [Int] -> Int
+settle opening limit fee =
+  foldl' (\balance tx ->
+           let next = balance + tx
+           in if tx < 0 && next < negate limit then next - fee
+              else next)
+        opening
diff --git a/pages/refactorings/extract-method/02-running-balance/Before.scala b/pages/refactorings/extract-method/02-running-balance/Before.scala
new file mode 100644
index 0000000..46918cd
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/Before.scala
@@ -0,0 +1,8 @@
+// Closing balance after a run of transactions; a debit that leaves
+// the account below its overdraft limit is charged a fee.
+object Before:
+  def settle(opening: Int, limit: Int, fee: Int, txs: List[Int]): Int =
+    txs.foldLeft(opening) { (balance, tx) =>
+      val next = balance + tx
+      if tx < 0 && next < -limit then next - fee else next
+    }
diff --git a/pages/refactorings/extract-method/02-running-balance/Spec.hs b/pages/refactorings/extract-method/02-running-balance/Spec.hs
new file mode 100644
index 0000000..1b917d0
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/Spec.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+genAmount, genLimit, genFee :: Gen Int
+genAmount = Gen.int (Range.linear (-30) 30)
+genLimit  = Gen.int (Range.linear 0 20)
+genFee    = Gen.int (Range.linear 1 20)
+
+prop_settle_agrees :: Property
+prop_settle_agrees = withTests 500 $ property $ do
+  opening <- forAll genAmount
+  limit   <- forAll genLimit
+  fee     <- forAll genFee
+  txs     <- forAll (Gen.list (Range.linear 0 20) genAmount)
+  Before.settle opening limit fee txs ===
+    After.settle opening limit fee txs
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("settle: Before == After", prop_settle_agrees)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/extract-method/02-running-balance/Spec.scala b/pages/refactorings/extract-method/02-running-balance/Spec.scala
new file mode 100644
index 0000000..d940b9a
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/Spec.scala
@@ -0,0 +1,32 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("settle: Before == After", settleAgrees).withTests(500),
+  )
+
+  val genAmount: Gen[Int] = Gen.int(Range.linear(-30, 30))
+  val genLimit: Gen[Int]  = Gen.int(Range.linear(0, 20))
+  val genFee: Gen[Int]    = Gen.int(Range.linear(1, 20))
+
+  def settleAgrees: Property =
+    for
+      opening <- genAmount.forAll
+      limit   <- genLimit.forAll
+      fee     <- genFee.forAll
+      txs     <- genAmount.list(Range.linear(0, 20)).forAll
+    yield Before.settle(opening, limit, fee, txs) ====
+      After.settle(opening, limit, fee, txs)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport("Props", t, r,
+      ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/extract-method/02-running-balance/diagram.svg b/pages/refactorings/extract-method/02-running-balance/diagram.svg
new file mode 100644
index 0000000..c7d265c
--- /dev/null
+++ b/pages/refactorings/extract-method/02-running-balance/diagram.svg
@@ -0,0 +1,42 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 300" role="img" aria-labelledby="d2-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d2-title">Extracting step from settle as a nested definition. Before: settle folds the transactions with an inline lambda whose free variables are limit and fee. After: step stays inside settle; limit and fee remain in scope and are captured, balance and tx are the parameters, and settle calls txs.foldLeft(opening)(step).</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="214" rx="4"/>
+    <rect x="428" y="36" width="336" height="214" rx="4"/>
+  </g>
+  <rect x="52" y="82" width="340" height="82" rx="3" fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3"/>
+  <rect x="452" y="72" width="288" height="92" rx="3" fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1"/>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">settle(opening, limit, fee, txs) =</text>
+    <text x="40" y="76">txs.foldLeft(opening) {</text>
+    <text x="52" y="96">(balance, tx) =&gt;</text>
+    <text x="64" y="114">val next = balance + tx</text>
+    <text x="64" y="132">if tx &lt; 0 &amp;&amp; next &lt; -limit</text>
+    <text x="64" y="150">then next - fee else next</text>
+    <text x="40" y="178">}</text>
+    <text x="28" y="202" opacity=".75">free in the lambda: limit, fee</text>
+    <text x="440" y="56">settle(opening, limit, fee, txs) =</text>
+    <text x="464" y="90" font-weight="600">def step(balance, tx) =</text>
+    <text x="476" y="108">val next = balance + tx</text>
+    <text x="476" y="126">if tx &lt; 0 &amp;&amp; next &lt; -limit</text>
+    <text x="476" y="144">then next - fee else next</text>
+    <text x="440" y="196">txs.foldLeft(opening)(step)</text>
+    <text x="440" y="220" opacity=".75">limit, fee — stay in scope, captured</text>
+    <text x="440" y="236" opacity=".75">balance, tx — the fold's arguments</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="96" r="7.5"/>
+    <circle cx="428" cy="196" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="100">1</text>
+    <text x="428" y="200">1</text>
+  </g>
+  <path d="M652 188 V168" fill="none" stroke="currentColor" stroke-width="1.2"/>
+  <path d="M648.5 168 L652 158 L655.5 168 Z" fill="currentColor"/>
+  <text x="640" y="180" fill="currentColor" font-size="12" text-anchor="end">step</text>
+</svg>
diff --git a/pages/refactorings/extract-method/03-expression-eval/After.hs b/pages/refactorings/extract-method/03-expression-eval/After.hs
new file mode 100644
index 0000000..653bc80
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/After.hs
@@ -0,0 +1,19 @@
+-- Evaluate an arithmetic expression; division by zero has no value.
+module After where
+
+data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Div Expr Expr
+  deriving Show
+
+eval :: Expr -> Maybe Int
+eval (Lit n)   = Just n
+eval (Add l r) = binary (\a b -> Just (a + b)) l r
+eval (Mul l r) = binary (\a b -> Just (a * b)) l r
+eval (Div l r) = binary (\a b -> if b == 0 then Nothing else Just (a `div` b)) l r
+
+-- Takes the operands unevaluated, so the right one is still only forced
+-- when the left one has a value, exactly as in Before.
+binary :: (Int -> Int -> Maybe Int) -> Expr -> Expr -> Maybe Int
+binary op l r = do
+  a <- eval l
+  b <- eval r
+  op a b
diff --git a/pages/refactorings/extract-method/03-expression-eval/After.scala b/pages/refactorings/extract-method/03-expression-eval/After.scala
new file mode 100644
index 0000000..c483134
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/After.scala
@@ -0,0 +1,19 @@
+// Evaluate an arithmetic expression; division by zero has no value.
+object After:
+  enum Expr:
+    case Lit(n: Int)
+    case Add(l: Expr, r: Expr)
+    case Mul(l: Expr, r: Expr)
+    case Div(l: Expr, r: Expr)
+  import Expr.*
+
+  def eval(e: Expr): Option[Int] = e match
+    case Lit(n)    => Some(n)
+    case Add(l, r) => binary(l, r)((a, b) => Some(a + b))
+    case Mul(l, r) => binary(l, r)((a, b) => Some(a * b))
+    case Div(l, r) => binary(l, r)((a, b) => Option.when(b != 0)(a / b))
+
+  // Takes the operands unevaluated, so the right one is still only evaluated
+  // when the left one has a value, exactly as in Before.
+  def binary(l: Expr, r: Expr)(op: (Int, Int) => Option[Int]): Option[Int] =
+    for a <- eval(l); b <- eval(r); c <- op(a, b) yield c
diff --git a/pages/refactorings/extract-method/03-expression-eval/Before.hs b/pages/refactorings/extract-method/03-expression-eval/Before.hs
new file mode 100644
index 0000000..90992ed
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/Before.hs
@@ -0,0 +1,20 @@
+-- Evaluate an arithmetic expression; division by zero has no value.
+module Before where
+
+data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Div Expr Expr
+  deriving Show
+
+eval :: Expr -> Maybe Int
+eval (Lit n)   = Just n
+eval (Add l r) = do
+  a <- eval l
+  b <- eval r
+  Just (a + b)
+eval (Mul l r) = do
+  a <- eval l
+  b <- eval r
+  Just (a * b)
+eval (Div l r) = do
+  a <- eval l
+  b <- eval r
+  if b == 0 then Nothing else Just (a `div` b)
diff --git a/pages/refactorings/extract-method/03-expression-eval/Before.scala b/pages/refactorings/extract-method/03-expression-eval/Before.scala
new file mode 100644
index 0000000..ae40269
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/Before.scala
@@ -0,0 +1,14 @@
+// Evaluate an arithmetic expression; division by zero has no value.
+object Before:
+  enum Expr:
+    case Lit(n: Int)
+    case Add(l: Expr, r: Expr)
+    case Mul(l: Expr, r: Expr)
+    case Div(l: Expr, r: Expr)
+  import Expr.*
+
+  def eval(e: Expr): Option[Int] = e match
+    case Lit(n)    => Some(n)
+    case Add(l, r) => for a <- eval(l); b <- eval(r) yield a + b
+    case Mul(l, r) => for a <- eval(l); b <- eval(r) yield a * b
+    case Div(l, r) => for a <- eval(l); b <- eval(r); if b != 0 yield a / b
diff --git a/pages/refactorings/extract-method/03-expression-eval/Spec.hs b/pages/refactorings/extract-method/03-expression-eval/Spec.hs
new file mode 100644
index 0000000..58c4dee
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/Spec.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+genExpr :: Gen Before.Expr
+genExpr = Gen.recursive Gen.choice
+  [ Before.Lit <$> Gen.int (Range.linear (-20) 20) ]
+  [ Gen.subterm2 genExpr genExpr Before.Add
+  , Gen.subterm2 genExpr genExpr Before.Mul
+  , Gen.subterm2 genExpr genExpr Before.Div
+  ]
+
+toAfter :: Before.Expr -> After.Expr
+toAfter (Before.Lit n)   = After.Lit n
+toAfter (Before.Add l r) = After.Add (toAfter l) (toAfter r)
+toAfter (Before.Mul l r) = After.Mul (toAfter l) (toAfter r)
+toAfter (Before.Div l r) = After.Div (toAfter l) (toAfter r)
+
+prop_eval_agrees :: Property
+prop_eval_agrees = property $ do
+  e <- forAll genExpr
+  Before.eval e === After.eval (toAfter e)
+
+-- A left operand without a value short-circuits: the right operand is never
+-- forced, before and after. (Division by zero has no value, so it does not throw here.)
+prop_short_circuit_preserved :: Property
+prop_short_circuit_preserved = property $ do
+  e <- forAll genExpr
+  Before.eval (Before.Add (Before.Div e (Before.Lit 0)) undefined) === Nothing
+  After.eval (After.Add (After.Div (toAfter e) (After.Lit 0)) undefined) === Nothing
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("eval: Before == After", prop_eval_agrees)
+    , ("short-circuit on a valueless left operand is preserved", prop_short_circuit_preserved)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/extract-method/03-expression-eval/Spec.scala b/pages/refactorings/extract-method/03-expression-eval/Spec.scala
new file mode 100644
index 0000000..dbe5c3a
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/Spec.scala
@@ -0,0 +1,46 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("eval: Before == After", evalAgrees),
+    property("dividing by zero has no value, never throws", divByZeroIsNone),
+  )
+
+  import Before.Expr, Before.Expr.*
+
+  val genLit: Gen[Expr] = Gen.int(Range.linear(-20, 20)).map(Lit(_))
+  def genExpr(depth: Int): Gen[Expr] =
+    if depth == 0 then genLit
+    else
+      val sub = genExpr(depth - 1)
+      Gen.choice1(
+        genLit,
+        for l <- sub; r <- sub yield Add(l, r),
+        for l <- sub; r <- sub yield Mul(l, r),
+        for l <- sub; r <- sub yield Div(l, r),
+      )
+
+  def toAfter(e: Expr): After.Expr = e match
+    case Lit(n)    => After.Expr.Lit(n)
+    case Add(l, r) => After.Expr.Add(toAfter(l), toAfter(r))
+    case Mul(l, r) => After.Expr.Mul(toAfter(l), toAfter(r))
+    case Div(l, r) => After.Expr.Div(toAfter(l), toAfter(r))
+
+  def evalAgrees: Property =
+    for e <- genExpr(4).forAll
+    yield Before.eval(e) ==== After.eval(toAfter(e))
+
+  def divByZeroIsNone: Property =
+    for e <- genExpr(3).forAll
+    yield Before.eval(Div(e, Lit(0))) ==== None and After.eval(toAfter(Div(e, Lit(0)))) ==== None
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default), t.result, Seed.fromTime())
+    println(Test.renderReport("Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/extract-method/03-expression-eval/diagram.svg b/pages/refactorings/extract-method/03-expression-eval/diagram.svg
new file mode 100644
index 0000000..91dff55
--- /dev/null
+++ b/pages/refactorings/extract-method/03-expression-eval/diagram.svg
@@ -0,0 +1,68 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 404" role="img" aria-labelledby="d3-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d3-title">Extracting binary from eval. Before: eval handles Add, Mul and Div with the same shape, for a from eval(l) and b from eval(r), differing only in the combining step. After: each case calls binary(l, r)(op) with the operands unevaluated and the combining step as op; binary evaluates l then r and applies op, calling back into eval.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="220" rx="4"/>
+    <rect x="428" y="36" width="336" height="180" rx="4"/>
+    <rect x="428" y="300" width="336" height="90" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="46" y="99" width="340" height="18" rx="3"/>
+    <rect x="46" y="135" width="340" height="18" rx="3"/>
+    <rect x="46" y="171" width="340" height="36" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">eval(e) = e match</text>
+    <text x="40" y="76">case Lit(n) =&gt; Some(n)</text>
+    <text x="40" y="94">case Add(l, r) =&gt;</text>
+    <text x="52" y="112">for a &lt;- eval(l); b &lt;- eval(r) yield a + b</text>
+    <text x="40" y="130">case Mul(l, r) =&gt;</text>
+    <text x="52" y="148">for a &lt;- eval(l); b &lt;- eval(r) yield a * b</text>
+    <text x="40" y="166">case Div(l, r) =&gt;</text>
+    <text x="52" y="184">for a &lt;- eval(l); b &lt;- eval(r); if b != 0</text>
+    <text x="52" y="202">yield a / b</text>
+    <text x="28" y="226" opacity=".75">the shape repeats three times; only the</text>
+    <text x="28" y="242" opacity=".75">combining step differs, and it becomes op</text>
+    <text x="440" y="58">eval(e) = e match</text>
+    <text x="452" y="76">case Lit(n) =&gt; Some(n)</text>
+    <text x="452" y="94">case Add(l, r) =&gt;</text>
+    <text x="464" y="112">binary(l, r)((a, b) =&gt; Some(a + b))</text>
+    <text x="452" y="130">case Mul(l, r) =&gt;</text>
+    <text x="464" y="148">binary(l, r)((a, b) =&gt; Some(a * b))</text>
+    <text x="452" y="166">case Div(l, r) =&gt;</text>
+    <text x="464" y="184">binary(l, r)((a, b) =&gt;</text>
+    <text x="476" y="202">Option.when(b != 0)(a / b))</text>
+    <text x="440" y="322" font-size="13" font-weight="600">binary(l, r)(op) =</text>
+    <text x="452" y="340">for a &lt;- eval(l); b &lt;- eval(r)</text>
+    <text x="476" y="358">c &lt;- op(a, b)</text>
+    <text x="452" y="376">yield c</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="99" r="7.5"/>
+    <circle cx="386" cy="135" r="7.5"/>
+    <circle cx="386" cy="171" r="7.5"/>
+    <circle cx="428" cy="300" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="103">1</text>
+    <text x="386" y="139">1</text>
+    <text x="386" y="175">1</text>
+    <text x="428" y="304">1</text>
+  </g>
+  <g fill="none" stroke="currentColor">
+    <path d="M460 216 V292" stroke-width="1.2"/>
+    <path d="M720 300 V224" stroke-width="1" stroke-dasharray="3 3"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M456.5 292 L460 300 L463.5 292 Z"/>
+    <path d="M716.5 224 L720 216 L723.5 224 Z"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="472" y="248">l, r <tspan opacity=".7">— the operands, unevaluated</tspan></text>
+    <text x="472" y="266">op <tspan opacity=".7">— the combining step</tspan></text>
+    <text x="710" y="290" text-anchor="end" opacity=".7">calls back: eval(l), eval(r)</text>
+  </g>
+</svg>
diff --git a/pages/refactorings/extract-method/diagrams/koan.svg b/pages/refactorings/extract-method/diagrams/koan.svg
new file mode 100644
index 0000000..892c237
--- /dev/null
+++ b/pages/refactorings/extract-method/diagrams/koan.svg
@@ -0,0 +1,34 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 640 184" role="img" aria-labelledby="koan-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="koan-title">Extract / Inline method: one equation read in two directions. Left: f x = … e …. Right: g v = e and f x = … g v …. The free variables of e are the parameters v — except where the definition stays nested, in which case v is just what lies outside that nested scope. The arrow to the right is extract (fold, lambda-lift); the arrow to the left is inline (unfold, beta).</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="28">before</text>
+    <text x="424" y="28">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="40" width="200" height="100" rx="4"/>
+    <rect x="424" y="40" width="200" height="100" rx="4"/>
+  </g>
+  <g fill="currentColor" font-size="14" text-anchor="middle">
+    <text x="116" y="76">f x = … <tspan font-style="italic" font-weight="700">e</tspan> …</text>
+    <text x="524" y="70">g <tspan font-style="italic" font-weight="700">v</tspan> = <tspan font-style="italic">e</tspan></text>
+    <text x="524" y="94">f x = … <tspan font-weight="700">g <tspan font-style="italic">v</tspan></tspan> …</text>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle" opacity=".75">
+    <text x="116" y="104"><tspan font-style="italic">e</tspan>: the region to extract</text>
+    <text x="116" y="122">free variables of <tspan font-style="italic">e</tspan>: <tspan font-style="italic">v</tspan></text>
+    <text x="524" y="122"><tspan font-style="italic">v</tspan>: the parameters of g</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M232 74 H398"/>
+    <path d="M408 110 H242"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M398 70.5 L406 74 L398 77.5 Z"/>
+    <path d="M242 106.5 L234 110 L242 113.5 Z"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="320" y="64">extract (define and fold / lambda-lift)</text>
+    <text x="320" y="128">inline (unfold and &beta;-reduce / denest)</text>
+  </g>
+  <text x="320" y="170" fill="currentColor" font-size="12" text-anchor="middle" opacity=".75"><tspan font-style="italic">v</tspan> are the free variables of <tspan font-style="italic">e</tspan>; they become the parameters of g</text>
+</svg>
diff --git a/pages/refactorings/extract-method/run.sh b/pages/refactorings/extract-method/run.sh
new file mode 100755
index 0000000..7b8cb88
--- /dev/null
+++ b/pages/refactorings/extract-method/run.sh
@@ -0,0 +1,24 @@
+#!/bin/sh
+# Runs every hedgehog property for this refactoring, in both languages.
+# Each NN-*/ directory holds Before + After + Spec in Scala 3 and Haskell;
+# Spec generates inputs and asserts Before and After agree on all of them.
+#
+# Needs: scala-cli (https://scala-cli.virtuslab.org) and either ghc with
+# hedgehog on the package path, or docker (the image is built on first use).
+set -eu
+cd "$(dirname "$0")"
+
+if command -v ghc >/dev/null 2>&1 && ghc-pkg list hedgehog 2>/dev/null | grep -q hedgehog; then
+  hs() { runghc -i"$1" "$1/Spec.hs"; }
+else
+  docker image inspect cp-hedgehog >/dev/null 2>&1 || \
+    printf 'FROM haskell:9.8-slim\nRUN cabal update && cabal install --lib hedgehog\n' | docker build -t cp-hedgehog -
+  hs() { docker run --rm -v "$PWD:/w" -w /w cp-hedgehog runghc -i"$1" "$1/Spec.hs"; }
+fi
+
+for d in [0-9][0-9]-*/; do
+  d=${d%/}
+  echo "== $d (scala)";   scala-cli run "$d" --main-class spec
+  echo "== $d (haskell)"; hs "$d"
+done
+echo "all properties passed"