| 123456789101112131415161718192021222324252627 |
- {-# OPTIONS --sized-types #-}
- open import Agda.Builtin.IO
- open import Agda.Builtin.Size
- open import Agda.Builtin.Unit
- data D (i : Size) : Set where
- {-# FOREIGN GHC
- data Empty i
- #-}
- {-# COMPILE GHC D = data Empty () #-}
- f : ∀ {i} → D i → D i
- f ()
- {-# COMPILE GHC f as f #-}
- postulate
- return : {A : Set} → A → IO A
- {-# COMPILE GHC return = \_ -> return #-}
- main : IO ⊤
- main = return _
|
