Agda 練習

あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。
agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。

module NList where

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + n     = n
(succ m) + n = succ (m + n)
_*_ : Nat -> Nat -> Nat
zero * _      = zero
(succ zero) * n = n
(succ m) * n    = m + (m * n)

data List (A : Set) : Nat -> Set where
   []   : List A zero
   _::_ : {n : Nat} -> A -> List A n -> List A (succ n)
   
head : {A : Set} {n : Nat} -> List A (succ n) -> A
head (x :: xs) = x
tail : {A : Set} {n : Nat} -> List A (succ n) -> List A n
tail (x :: xs) = xs
take : {A : Set} {m : Nat} -> (n : Nat) -> List A (n + m) -> List A n
take zero _ = []
take (succ n) (x :: xs) = x :: take n xs
drop : {A : Set} {m : Nat} -> (n : Nat) -> List A (n + m) -> List A m
drop zero l = l
drop (succ n) (x :: xs) = drop n xs

one = succ zero
two = succ one
three = succ two

x = drop three (zero :: (one :: (two :: [])))
y = take two (zero :: (one :: (two :: [])))

agda のコードはハイライトされないのかー。