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 のコードはハイライトされないのかー。