--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.hgignore	Thu Feb 20 19:52:51 2020 +0900
@@ -0,0 +1,10 @@
+syntax:glob
+
+# Created by https://www.gitignore.io/api/agda
+# Edit at https://www.gitignore.io/?templates=agda
+
+### Agda ###
+*.agdai
+MAlonzo/**
+
+# End of https://www.gitignore.io/api/agda

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/day.agda	Thu Feb 20 19:52:51 2020 +0900
@@ -0,0 +1,99 @@
+module day where
+
+data day : Set where
+  monday : day
+  tuesday : day
+  wednesday : day
+  thursday : day
+  friday : day
+  saturday : day
+  sunday : day
+
+-- ↑はただのデータ
+
+nextWeekday : day → day
+nextWeekday monday = tuesday
+nextWeekday tuesday = wednesday
+nextWeekday wednesday = thursday
+nextWeekday thursday = friday
+nextWeekday friday = monday
+nextWeekday saturday = monday
+nextWeekday sunday = monday
+
+hoge : day → day
+hoge x = nextWeekday x
+
+data bool : Set where
+  true : bool
+  false : bool
+
+negb : bool → bool
+negb true = false
+negb false = true
+
+andb : bool → bool → bool
+-- andb true true = true
+-- andb true false = false
+-- andb false true = false
+-- andb false false = false
+andb true b = b
+andb false _ = false
+
+orb : (x y : bool) → bool
+orb true _ = true
+orb false y = y
+
+data _≡_  {a} { A : Set a} ( x : A ) : A → Set a where
+  refl : x ≡ x
+
+testOrb1 : (orb true false) ≡ true
+testOrb1 = refl
+
+data nat : Set where
+  O :  nat
+  Succ : nat → nat
+
+pred : nat → nat
+pred O = O
+pred (Succ x) = x
+
+minustwo : nat → nat
+minustwo x = pred (pred x)
+
+evenb : nat → bool
+evenb O = true
+evenb (Succ O) = false
+evenb (Succ (Succ x)) = evenb x
+
+open import Data.Nat.Base
+
+factorial : ℕ → ℕ
+factorial zero = 1
+factorial (suc x) = x * (factorial (x))
+
+beqNat : ℕ  → ℕ  → bool
+beqNat zero zero = true
+beqNat zero (suc y) = false 
+beqNat (suc x) zero = false 
+beqNat (suc x) (suc y) = beqNat x y
+
+-- beqNat x y with x | y 
+-- beqNat x y | zero | zero = true
+-- beqNat x y | zero | suc a = false
+-- beqNat x y | suc z | zero = false
+-- beqNat x y | suc z | suc a = beqNat z a 
+
+open import Data.Nat.Properties 
+open import Data.Empty
+
+n+0 : ( n : ℕ ) →  ( n + 0 ) ≡ n
+n+0 zero = refl
+n+0 (suc x) rewrite  (  +-comm (suc x) 0 ) = refl
+
+andbTrueElim2 : ( b c : bool ) →  (andb b c ) ≡ true → c ≡ true
+-- andbTrueElim2 true c d with d
+-- andbTrueElim2 true .true d | refl = refl
+andbTrueElim2 _ true d = refl
+andbTrueElim2 false false ()
+andbTrueElim2 true false ()
+