Mercurial > hg > Members > atton > delta_monad
diff agda/basic.agda @ 28:6e6d646d7722
Split basic functions to file
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 14:55:40 +0900 |
parents | |
children | e0ba1bf564dd |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/basic.agda Tue Oct 07 14:55:40 2014 +0900 @@ -0,0 +1,10 @@ +module basic where + +id : {A : Set} -> A -> A +id x = x + +_∙_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C) +f ∙ g = \x -> g (f x) + +postulate String : Set +postulate show : {A : Set} -> A -> String \ No newline at end of file