--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Agda/tutorial.md	Wed Dec 16 14:05:01 2020 +0900
@@ -0,0 +1,42 @@
+# Agda入門
+
+間違いもあると思うが一応記録していく。
+
+## 基本動作
+基本的なコードを以下に記載する。
+
+```agda:hello.agda
+module hello where
+
+test1 : Set → Set
+test1  x = x
+```
+
+書いた定義を
+C-c C-l でコンパイルすることができる。
+
+書いたコードの解説をすると、
+- `module hello where`は必要な宣言で、`module`の次にファイル名を記述する。
+- `test :`の行は関数の宣言と仕様の記述をしている。
+    - `:`の前で関数名を定義している
+    - `:`の後で仕様の記述をしている。
+        - 意味はこの関数は**型**がSetの引数を受けとり、返り値として**型**がSetのものを返す。
+- `test =`の行は関数の実装を記述している。
+    - `=`の前にxがあるが、これは関数が引数としてxを受け取ったことを表している。
+        - 余談だがHaskellでも同じように関数の後ろに引数を記述する。
+    - 仕様として、引数で受け取った物をそのまま返しても成り立つ
+        - Setを受け取りSetを返すだけなのでこれで良い
+
+また、`=`から後方を削除し、`?`を入力しC-c C-lすることもできる。その際に`{ }`が表示される。
+- その中でC-c C-, すると引数に何が格納されているのか見ることができる。
+- また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。
+
+コマンド群は[ここ](https://agda.wiki.fc2.com/wiki/コマンド一覧)にも記載されている。
+
+## 関数定義
+
+
+## data型
+
+
+## record型
\ No newline at end of file