diff --git a/examples/hello.quox b/examples/hello.quox
new file mode 100644
index 0000000..e1f2052
--- /dev/null
+++ b/examples/hello.quox
@@ -0,0 +1,26 @@
+def0 Unit : ★ = {tt}
+
+def drop-unit : 0.(A : ★) → Unit → A → A =
+  λ A u x ⇒ case u return A of {'tt ⇒ x}
+
+-- postulate0 IOState : ★
+
+def0 IO : ★ → ★ = λ A ⇒ IOState → A × IOState
+
+def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
+  λ A B m k s0 ⇒
+  case m s0 return B × IOState of { (x, s1) ⇒ k x s1 }
+
+def seq : IO Unit → IO Unit → IO Unit =
+  λ a b ⇒ bind Unit Unit a (λ u ⇒ drop-unit (IO Unit) u b)
+
+#[compile-scheme "(lambda (n) (builtin-io (display n) (newline) 'tt))"]
+postulate print-ℕ : ℕ → IO Unit
+
+#[compile-scheme "(lambda (str) (builtin-io (display str) (newline) 'tt))"]
+postulate print : String → IO Unit
+
+load "nat.quox"
+
+#[main]
+def main = seq (print-ℕ (nat.plus 1000000000 1)) (print "(nice)")