--- a/Agda/tutorial.md	Wed Dec 16 15:04:03 2020 +0900
+++ b/Agda/tutorial.md	Wed Dec 16 15:11:16 2020 +0900
@@ -31,12 +31,130 @@
 - その中でC-c C-, すると引数に何が格納されているのか見ることができる。
 - また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。
 
+関数を実行したい際にはC-c C-n で実行することができる。
+
 コマンド群は[ここ](https://agda.wiki.fc2.com/wiki/コマンド一覧)にも記載されている。
+特殊文字などもみんなのagdaに記載されている。
 
 ## 関数定義
+関数定義の際に基本となる記述を記載しておく。
 
+```agda:func.agda
+test2 : (A : Set) → Set
+test2 a = a
+
+-- 引数を増やすこともできる。
+test3 : (A B : Set) → Set
+test3 a b = b
+
+-- ()ではなく{}で方を定義することもできる。その場合{}で定義した部分の変数を隠すことができる。
+test4 : {A B : Set} → A → (A → B) → B
+test4 a x = x a
+
+-- {}で定義した部分を取得することも可能
+test5 : {A B : Set} → A → (A → B) → B
+test5 {A} {B} a x = x a
+
+-- 上記の{}で定義した物を()で書き換えると以下のようになる
+test6 : (A B : Set) → A → (A → B) → B
+test6 A B a x = x a
+-- あまりスマートではないし定義の意味が{}で記述した場合と違う
+```
 
 ## data型
 
+```agda:data.agda
+-- 次はdata型とrecord型の説明
+-- 記号などはみんなのagdaにほとんど載っていたり、普通にググっても出る。
 
-## record型
\ No newline at end of file
+data _∨_ (A B : Set) : Set where
+  front : A → A ∨ B
+  back  : B → A ∨ B
+-- 関数名として_∨_を定義しているが、これで中置演算子を定義することができる。
+-- 実際にやっていることは下記に定義している関数と同じ
+
+data or (A B : Set) : Set where
+  front : A → or A B
+  back  : B → or A B
+```
+data型というのは分岐のことであり、「どちらか一方が必ず動作する。」ということになる。
+
+わかり易い例としてBool型の定義がある。
+```
+data Bool : Set where
+  true  : Bool
+  false : Bool
+```
+data型を使用した例としてジャンケンを定義してみる。
+```agda:rps.agda
+data hand : Set where
+  r : hand
+  p : hand
+  s : hand
+
+-- 「手」を二つ受け取って勝った方の手を返すように設計すると
+-- 定義は「handを2つ受け取る。最終的にhandを返す」となり、以下のようになる。
+rps : (A B : hand) → hand
+-- rps : hand → hand → hand これでも良い
+-- rps : (_ _ : hand) → hand これでもできるかもしれない 
+rps r r = r
+rps r p = p
+rps r s = r
+rps p r = p
+rps p p = p
+rps p s = s
+rps s r = r
+rps s p = s
+rps s s = s
+```
+場合分けの数が足りない場合、agdaが親切に怒ってくれる。
+
+
+## record型
+data型とは違い、
+オブジェクトあるいは構造体のようなもの。  
+以下の関数はAND。p1で前方部分が取得でき、p2で後方部分が取得できる。
+
+``` agda:record.agda
+record _∧_ (A B : Set) : Set where
+  field
+    p1 : A
+    p2 : B
+
+-- 普通にANDの後ろの方を取得することもできる
+datatest1 : {A B C : Set} → (A ∧ (B → C )) → (B → C)
+datatest1 x b = _∧_.p2 x b
+
+
+-- ANDの後ろの方を取得した結果を使用することもできる。
+datatest : {A B C : Set} → B → (A ∧ (B → C )) → C
+datatest b x = _∧_.p2 x b
+```
+
+これらを使用して三段論法を定義することができる。  
+定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
+```
+syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
+syllogism x a = _∧_.p2 x (_∧_.p1 x a)
+```
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+