Mercurial > hg > Members > atton > similar_monad
comparison agda/list.agda @ 31:33b386de3f56
Proof list-associative
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 18 Oct 2014 13:38:29 +0900 |
parents | 5ba82f107a95 |
children | 743c05b98dad |
comparison
equal
deleted
inserted
replaced
30:c2f40b6d4027 | 31:33b386de3f56 |
---|---|
23 empty-append (x :: xs) = begin | 23 empty-append (x :: xs) = begin |
24 x :: (xs ++ []) | 24 x :: (xs ++ []) |
25 ≡⟨ cong (_::_ x) (empty-append xs) ⟩ | 25 ≡⟨ cong (_::_ x) (empty-append xs) ⟩ |
26 x :: xs | 26 x :: xs |
27 ∎ | 27 ∎ |
28 | |
29 | |
30 list-associative : {A : Set} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c) | |
31 list-associative [] b c = refl | |
32 list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c) |