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