Issue2914.agda 206 B

12345678910111213141516
  1. open import Agda.Builtin.IO
  2. open import Agda.Builtin.Nat
  3. open import Agda.Builtin.Unit
  4. private
  5. n : Nat
  6. n = 7
  7. {-# COMPILE GHC n as n #-}
  8. postulate
  9. main : IO ⊤
  10. {-# COMPILE GHC main = print n #-}