[Moved the one-constructor unit type to Data.Unit. Nils Anders Danielsson **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 () () #-}