diff --git a/TODO.md b/TODO.md
index 5091e08..5c271a1 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,10 +2,7 @@
 
 > 支持直接递归函数与相互递归函数，不能判断等价的地方就不判断。
 
-[lang0] `occurCheck` -- a pass to create `FnRecursive` from `Fn`
-
-- only in the same module for now
-
+[lang0] `assertEqual` & `assertNotEqual` improve error message
 [lang0] `equivalent` -- `FnRecursive`
 [lang0] `equivalentNeutral` -- `ApRecursive`
 
diff --git a/docs/lang0/examples/factorial.scm b/docs/lang0/examples/factorial.scm
new file mode 100644
index 0000000..8500a3e
--- /dev/null
+++ b/docs/lang0/examples/factorial.scm
@@ -0,0 +1,18 @@
+(import "./nat-church.scm" zero? add mul sub1)
+(import "./nat-church.scm" zero one two three four)
+(import "./boolean.scm" if true false)
+
+;; (claim factorial (-> Nat Nat))
+
+(define (factorial n)
+  (if (zero? n)
+    one
+    (mul n (factorial (sub1 n)))))
+
+factorial
+
+(assert-equal (factorial zero) one)
+(assert-equal (factorial one) one)
+(assert-equal (factorial two) two)
+(assert-equal (factorial three) (mul three two))
+(assert-equal (factorial four) (mul four (mul three two)))
diff --git a/docs/lang0/examples/nat-even-odd.scm b/docs/lang0/examples/nat-even-odd.scm
index ce9da9e..dd7f426 100644
--- a/docs/lang0/examples/nat-even-odd.scm
+++ b/docs/lang0/examples/nat-even-odd.scm
@@ -3,21 +3,13 @@
 (import "./nat-church.scm" one two three four)
 (import "./fix.scm" Y)
 
-(define even?
-  (let ([wrap (lambda (even?)
-                (lambda (n)
-                  (if (zero? n) true
-                      (if (zero? (sub1 n)) false
-                          (even? (sub1 (sub1 n)))))))])
-    (Y wrap)))
+(define (even? n)
+  (if (zero? n) true
+      (odd? (sub1 n))))
 
-(define odd?
-  (let ([wrap (lambda (odd?)
-                (lambda (n)
-                  (if (zero? n) false
-                      (if (zero? (sub1 n)) true
-                          (odd? (sub1 (sub1 n)))))))])
-    (Y wrap)))
+(define (odd? n)
+  (if (zero? n) false
+      (even? (sub1 n))))
 
 (assert-equal
   (even? zero)
diff --git a/package-lock.json b/package-lock.json
index 39da29b..9d8cf63 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -12,7 +12,8 @@
         "@cicada-lang/framework": "^0.2.0",
         "@cicada-lang/sexp": "^0.1.2",
         "@xieyuheng/command-line": "^0.1.2",
-        "@xieyuheng/ty": "^0.2.1"
+        "@xieyuheng/ty": "^0.2.1",
+        "dedent": "^1.5.1"
       },
       "bin": {
         "clique": "bin/clique.js"
@@ -272,6 +273,19 @@
       "resolved": "https://registry.npmjs.org/core-util-is/-/core-util-is-1.0.3.tgz",
       "integrity": "sha512-ZQBvi1DcpJ4GDqanjucZ2Hj3wEO5pZDS89BWbkcrvdxksJorwUDDZamX9ldFkp9aw2lmBDLgkObEA4DWNJ9FYQ=="
     },
+    "node_modules/dedent": {
+      "version": "1.5.1",
+      "resolved": "https://registry.npmjs.org/dedent/-/dedent-1.5.1.tgz",
+      "integrity": "sha512-+LxW+KLWxu3HW3M2w2ympwtqPrqYRzU8fqi6Fhd18fBALe15blJPI/I4+UHveMVG6lJqB4JNd4UG0S5cnVHwIg==",
+      "peerDependencies": {
+        "babel-plugin-macros": "^3.1.0"
+      },
+      "peerDependenciesMeta": {
+        "babel-plugin-macros": {
+          "optional": true
+        }
+      }
+    },
     "node_modules/define-data-property": {
       "version": "1.1.4",
       "resolved": "https://registry.npmjs.org/define-data-property/-/define-data-property-1.1.4.tgz",
diff --git a/package.json b/package.json
index 0acb74f..fbf8ef7 100644
--- a/package.json
+++ b/package.json
@@ -28,7 +28,8 @@
     "@cicada-lang/framework": "^0.2.0",
     "@cicada-lang/sexp": "^0.1.2",
     "@xieyuheng/command-line": "^0.1.2",
-    "@xieyuheng/ty": "^0.2.1"
+    "@xieyuheng/ty": "^0.2.1",
+    "dedent": "^1.5.1"
   },
   "devDependencies": {
     "@types/node": "^20.12.4",
diff --git a/src/lang0/run/occurCheck.ts b/src/lang0/run/occurCheck.ts
index 2a0fcfe..533ca46 100644
--- a/src/lang0/run/occurCheck.ts
+++ b/src/lang0/run/occurCheck.ts
@@ -1,6 +1,29 @@
+import dedent from "dedent"
 import type { Definition } from "../definition/Definition.js"
+import { expIndirectFreeNames } from "../exp/expIndirectFreeNames.js"
+import * as Exps from "../exp/index.js"
+import { formatExp } from "../format/formatExp.js"
 import type { Mod } from "../mod/index.js"
 
 export function occurCheck(mod: Mod, definition: Definition): void {
-  // TODO
+  const indirectFreeNames = expIndirectFreeNames(mod, definition.exp)
+
+  if (!indirectFreeNames.has(definition.name)) return
+
+  if (definition.exp["@kind"] !== "Fn") {
+    throw new Error(
+      dedent`
+        [occurCheck] Only function can be recursive
+
+          non-function exp: ${formatExp(definition.exp)}
+          recursive name: ${definition.name}
+        `,
+    )
+  }
+
+  definition.exp = Exps.FnRecursive(
+    definition.name,
+    definition.exp.name,
+    definition.exp.ret,
+  )
 }
diff --git a/src/lang0/run/runMod.ts b/src/lang0/run/runMod.ts
index 69444ac..e1aadb5 100644
--- a/src/lang0/run/runMod.ts
+++ b/src/lang0/run/runMod.ts
@@ -1,8 +1,8 @@
 import { modOwnDefinitions, type Mod } from "../mod/index.js"
 import { assertAllNamesDefined } from "./assertAllNamesDefined.js"
-import { occurCheck } from "./occurCheck.js"
 import { define } from "./define.js"
 import { execute } from "./execute.js"
+import { occurCheck } from "./occurCheck.js"
 
 export function runMod(mod: Mod): void {
   if (mod.isFinished) return