Mercurial > hg > Members > atton > delta_monad

diff 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
line wrap: on
line diff
--- a/agda/list.agda	Tue Oct 07 10:38:57 2014 +0900
+++ b/agda/list.agda	Tue Oct 07 14:43:33 2014 +0900
@@ -14,6 +14,9 @@
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
+[[_]] : {A : Set} -> A -> List A
+[[ x ]] = x :: []
+
 
 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
 empty-append [] = refl