# 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型