Mercurial > hg > Document > Growi
comparison Agda/tutorial.md @ 0:e12992dca4a0
init from Growi
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Dec 2020 14:05:01 +0900 |
| parents | |
| children | b6c284fd5ae4 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:e12992dca4a0 |
|---|---|
| 1 # Agda入門 | |
| 2 | |
| 3 間違いもあると思うが一応記録していく。 | |
| 4 | |
| 5 ## 基本動作 | |
| 6 基本的なコードを以下に記載する。 | |
| 7 | |
| 8 ```agda:hello.agda | |
| 9 module hello where | |
| 10 | |
| 11 test1 : Set → Set | |
| 12 test1 x = x | |
| 13 ``` | |
| 14 | |
| 15 書いた定義を | |
| 16 C-c C-l でコンパイルすることができる。 | |
| 17 | |
| 18 書いたコードの解説をすると、 | |
| 19 - `module hello where`は必要な宣言で、`module`の次にファイル名を記述する。 | |
| 20 - `test :`の行は関数の宣言と仕様の記述をしている。 | |
| 21 - `:`の前で関数名を定義している | |
| 22 - `:`の後で仕様の記述をしている。 | |
| 23 - 意味はこの関数は**型**がSetの引数を受けとり、返り値として**型**がSetのものを返す。 | |
| 24 - `test =`の行は関数の実装を記述している。 | |
| 25 - `=`の前にxがあるが、これは関数が引数としてxを受け取ったことを表している。 | |
| 26 - 余談だがHaskellでも同じように関数の後ろに引数を記述する。 | |
| 27 - 仕様として、引数で受け取った物をそのまま返しても成り立つ | |
| 28 - Setを受け取りSetを返すだけなのでこれで良い | |
| 29 | |
| 30 また、`=`から後方を削除し、`?`を入力しC-c C-lすることもできる。その際に`{ }`が表示される。 | |
| 31 - その中でC-c C-, すると引数に何が格納されているのか見ることができる。 | |
| 32 - また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。 | |
| 33 | |
| 34 コマンド群は[ここ](https://agda.wiki.fc2.com/wiki/コマンド一覧)にも記載されている。 | |
| 35 | |
| 36 ## 関数定義 | |
| 37 | |
| 38 | |
| 39 ## data型 | |
| 40 | |
| 41 | |
| 42 ## record型 |