Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://agda.github.io/agda-stdlib/master/System.Exit.Primitive.html below:

System.Exit.Primitive

------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive System.Exit simple bindings to Haskell functions
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module System.Exit.Primitive where

open import Agda.Builtin.Int using (Int)
open import Agda.Builtin.IO using (IO)

data ExitCode : Set where
  ExitSuccess : ExitCode
  ExitFailure : Int → ExitCode

{-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
{-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}

{-# FOREIGN GHC import qualified System.Exit as SE #-}

{-# FOREIGN GHC
toExitCode :: AgdaExitCode -> SE.ExitCode
toExitCode AgdaExitSuccess = SE.ExitSuccess
toExitCode (AgdaExitFailure n) = SE.ExitFailure (fromIntegral n)

fromExitCode :: SE.ExitCode -> AgdaExitCode
fromExitCode SE.ExitSuccess = AgdaExitSuccess
fromExitCode (SE.ExitFailure n) = AgdaExitFailure (fromIntegral n)
#-}

postulate
  exitWith : ∀ {a} {A : Set a} → ExitCode → IO A

{-# COMPILE GHC exitWith = \ _ _ -> SE.exitWith . toExitCode #-}

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4