| 12345678910111213141516171819 |
- open import Agda.Builtin.IO
- open import Agda.Builtin.Reflection
- open import Agda.Builtin.Strict
- open import Agda.Builtin.String
- open import Agda.Builtin.Unit
- postulate
- putStr : String → IO ⊤
- {-# FOREIGN GHC import qualified Data.Text.IO #-}
- {-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
- {-# COMPILE JS putStr =
- function (x) {
- return function(cb) {
- process.stdout.write(x); cb(0); }; } #-}
- main : IO ⊤
- main = primForce commitTC λ _ → putStr "Success\n"
|
