A1.agda

module A1 where


-- Bool 型
data Bool : Set where
  true : Bool
  false : Bool

-- パターンマッチや中値記法
_or_ : Bool -> Bool -> Bool 
true or b = true
false or true = true
false or false = false

_and_ : Bool -> Bool -> Bool
true and true = true
true and false = true
false and b = false

f : Bool -> Bool
f =  _or_ false

test1 : Bool
test1 = f true

-- zeroがNat型ということ、および、xがNat型ならsucc x もNat型だということを示している
data Nat : Set where 
   zero : Nat
   suc : Nat -> Nat


plus : Nat -> Nat -> Nat
plus zero n = n
plus (suc m) n = suc (plus m n)

_+_ : Nat -> Nat -> Nat
n + m = plus n m

data _≡_ {A : Set} (x : A) : A → Set where
   refl : x ≡ x


cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → (f x) ≡ (f y)
cong f refl = refl

unitPlus : (n : Nat) → (n + zero) ≡ n
unitPlus zero = refl
unitPlus (suc n) = cong suc (unitPlus n)

assocPlus : (l m n : Nat) → ((l + m) + n) ≡ (l + (m + n))
assocPlus zero m n = refl
assocPlus (suc l) m n = cong suc (assocPlus l m n)


transPlus : {A : Set} (l m n : A) → l ≡ m → m ≡ n → l ≡ n
transPlus l .l .l refl refl = refl


data Vec (A : Set) : Nat -> Set where
   [] : Vec A zero
   _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

-- 長さが 1 のNat型のリスト

test2 : Vec Nat (suc zero)
test2 = (suc zero) :: []

-- 長さが2のBool型のリスト
test3 : Vec Bool (suc (suc zero))
test3 = (λ x → x) (true :: (false :: []))