diff --git a/examples/refinement.html.pm b/examples/refinement.html.pm
new file mode 100644
index 0000000..8c32ab7
--- /dev/null
+++ b/examples/refinement.html.pm
@@ -0,0 +1,11 @@
+#lang pollen
+
+◊p{
+   As students learn to work with invariants, it is helpful and
+   instructive to express them directly in the source program. Pyret
+   supports ◊em{refinments} to enable this. Currently, refinements in
+   Pyret are checked dynamically, so that students don't have to go
+   through the hurdles of convincing a proof-assistant that the
+   program is compliant, and they can get concrete examples of
+   failures.
+   }
diff --git a/examples/refinement.js b/examples/refinement.js
new file mode 100644
index 0000000..57d384b
--- /dev/null
+++ b/examples/refinement.js
@@ -0,0 +1,44 @@
+const example = `use context starter2024
+
+fun is-sorted-ascending(l :: List<Number>) -> Boolean:
+  cases (List) l:
+    | empty => true
+    | link(f, r) =>
+      cases (List) r:
+        | empty => true
+        | link(fr, rr) =>
+          if f <= fr:
+            is-sorted-ascending(r)
+          else:
+            false
+          end
+      end
+  end
+end
+
+fun insert(n :: Number,
+    l :: List%(is-sorted-ascending))
+  -> List%(is-sorted-ascending):
+  cases (List) l:
+    | empty => [list: n]
+    | link(f, r) =>
+      if n < f: link(n, l)
+      else:     link(f, insert(n, r))
+      end
+  end
+end
+
+check:
+  insert(1, [list: 2, 3, 4]) is [list: 1, 2, 3, 4]
+  insert(1, [list: 3, 2, 4]) raises "predicate"
+end
+
+# Uncomment and run the next line to see the error message!
+# insert(1, [list: 3, 2, 4])
+`;
+
+export const refinement = {
+  definitionsAtLastRun: example,
+  editorContents: example,
+  replContents: ""
+};
diff --git a/index.html.pm b/index.html.pm
index 701a555..4b209c2 100644
--- a/index.html.pm
+++ b/index.html.pm
@@ -14,6 +14,7 @@
 		    ("tables" . "Tables")
 		    ("data" . "Data Structures")
 		    ("lambdas" . "Lambdas")
+		    ("refinement" . "Type Refinements")
 		    ("oop" . "Object-Oriented Programming")
 		    ("forloops" . "Loops")
 		    ("mutation" . "Mutation and State")