[Moved the one-constructor unit type to Data.Unit.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080617171430] hunk ./Data/Unit.agda 23
+
+-- A one-constructor unit type is useful for the FFI.
+
+data Unit : Set where
+  unit : Unit
+
+{-# COMPILED_DATA Unit () () #-}
hunk ./IO.agda 39
-
--- The types of writeFile and putStrLn were wrong (there was no COMPILED directives
--- for ⊤ and at the moment there can't be since it's a record). They return
--- something in the Haskell unit type. You probably want to move this somewhere else...
-data Unit : Set where
-  unit : Unit
-
-{-# COMPILED_DATA Unit () () #-}