From dda6e05eb34f6740a963c4feb88342cc9d2d2cb0 Mon Sep 17 00:00:00 2001
From: Shunsuke Shibayama <sbym1346@gmail.com>
Date: Mon, 14 Nov 2022 00:17:19 +0900
Subject: [PATCH 1/3] Create const_fn.er

---
 tests/const_fn.er | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/const_fn.er

diff --git a/tests/const_fn.er b/tests/const_fn.er
new file mode 100644
index 000000000..12ad9d062
--- /dev/null
+++ b/tests/const_fn.er
@@ -0,0 +1,7 @@
+Fib: Nat -> Nat
+Fib 0 = 0
+Fib 1 = 1
+Fib n = Fib(n-1) + Fib(n-2)
+
+fib10 = Fib 10
+fib10: {55}

From ccd81752f69fde4b7538869849e5b3be9828d99b Mon Sep 17 00:00:00 2001
From: Shunsuke Shibayama <sbym1346@gmail.com>
Date: Mon, 14 Nov 2022 00:42:02 +0900
Subject: [PATCH 2/3] Update const_fn.er

---
 tests/const_fn.er | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tests/const_fn.er b/tests/const_fn.er
index 12ad9d062..241edf87c 100644
--- a/tests/const_fn.er
+++ b/tests/const_fn.er
@@ -1,7 +1,6 @@
-Fib: Nat -> Nat
 Fib 0 = 0
 Fib 1 = 1
-Fib n = Fib(n-1) + Fib(n-2)
+Fib N: Nat = Fib(N-1) + Fib(N-2)
 
-fib10 = Fib 10
-fib10: {55}
+Fib10 = Fib 10
+Fib10: {55}

From d841cef2345374e472e7f30f4dd667c88a95e9d7 Mon Sep 17 00:00:00 2001
From: Shunsuke Shibayama <sbym1346@gmail.com>
Date: Mon, 14 Nov 2022 00:59:55 +0900
Subject: [PATCH 3/3] Update docs

---
 doc/JA/syntax/04_function.md | 12 +++++++-----
 tests/const_fn.er            |  1 +
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/doc/JA/syntax/04_function.md b/doc/JA/syntax/04_function.md
index b7a9e8f88..cb6e66ec2 100644
--- a/doc/JA/syntax/04_function.md
+++ b/doc/JA/syntax/04_function.md
@@ -234,12 +234,16 @@ factorial(-1) == -1 * factorial(-2) == -1 * -2 * factorial(-3) == ...
 そのかわり、計算をコンパイル時に行うことができるというメリットがあります。
 
 ```python
-Add(X, Y: Nat): Nat = X + Y
-assert Add(1, 2) == 3
+Add(X, Y: Nat) = X + Y
+Add: |X: Nat, Y: Nat|({X}, {Y}) -> {Add(X, Y)}
+Three = Add(1, 2)
+Three: {3}
 
 Factorial 0 = 1
 Factorial(X: Nat): Nat = X * Factorial(X - 1)
-assert Factorial(10) == 3628800
+Factorial: |X: Nat|{X} -> {Factorial(X)}
+Fact10 = Factorial(10)
+Fact10: {3628800}
 
 math = import "math"
 Sin X = math.sin X # ConstantError: this function is not computable at compile time
@@ -289,8 +293,6 @@ f(a, b) # TypeError: f() takes 1 positional argument but 2 were given
 f((a, b)) # OK
 ```
 
-関数型`T -> U`は実際のところ、`(T,) -> U`の糖衣構文です。
-
 <p align='center'>
     <a href='./03_declaration.md'>Previous</a> | <a href='./05_builtin_funcs.md'>Next</a>
 </p>
diff --git a/tests/const_fn.er b/tests/const_fn.er
index 241edf87c..49b80b53f 100644
--- a/tests/const_fn.er
+++ b/tests/const_fn.er
@@ -1,3 +1,4 @@
+# Fib: |N: Nat| {N} -> {Fib N}
 Fib 0 = 0
 Fib 1 = 1
 Fib N: Nat = Fib(N-1) + Fib(N-2)