Mercurial > hg > Members > atton > delta_monad

comparison agda/list.agda @ 26:5ba82f107a95

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define Similar in Agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Oct 2014 14:43:33 +0900
parents a5aadebc084d
children 33b386de3f56
comparison
equal deleted inserted replaced
25:a5aadebc084d 26:5ba82f107a95
12 infixl 30 _++_ 12 infixl 30 _++_
13 _++_ : {A : Set} -> List A -> List A -> List A 13 _++_ : {A : Set} -> List A -> List A -> List A
14 [] ++ ys = ys 14 [] ++ ys = ys
15 (x :: xs) ++ ys = x :: (xs ++ ys) 15 (x :: xs) ++ ys = x :: (xs ++ ys)
16 16
17 [[_]] : {A : Set} -> A -> List A
18 [[ x ]] = x :: []
19
17 20
18 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs 21 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
19 empty-append [] = refl 22 empty-append [] = refl
20 empty-append (x :: xs) = begin 23 empty-append (x :: xs) = begin
21 x :: (xs ++ []) 24 x :: (xs ++ [])