------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive System.Random simple bindings to Haskell functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module System.Random.Primitive where
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.Float using (Float)
open import Agda.Builtin.Int using (Int)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Word using (Word64)
open import Foreign.Haskell.Pair using (Pair)
postulate
randomIO-Char : IO Char
randomRIO-Char : Pair Char Char → IO Char
randomIO-Int : IO Int
randomRIO-Int : Pair Int Int → IO Int
randomIO-Float : IO Float
randomRIO-Float : Pair Float Float → IO Float
randomIO-Nat : IO Nat
randomRIO-Nat : Pair Nat Nat → IO Nat
randomIO-Word64 : IO Word64
randomRIO-Word64 : Pair Word64 Word64 → IO Word64
{-# FOREIGN GHC import System.Random #-}
{-# COMPILE GHC randomIO-Char = randomIO #-}
{-# COMPILE GHC randomRIO-Char = randomRIO #-}
{-# COMPILE GHC randomIO-Int = randomIO #-}
{-# COMPILE GHC randomRIO-Int = randomRIO #-}
{-# COMPILE GHC randomIO-Float = randomIO #-}
{-# COMPILE GHC randomRIO-Float = randomRIO #-}
{-# COMPILE GHC randomIO-Nat = abs <$> randomIO #-}
{-# COMPILE GHC randomRIO-Nat = randomRIO #-}
{-# COMPILE GHC randomIO-Word64 = randomIO #-}
{-# COMPILE GHC randomRIO-Word64 = randomRIO #-}
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