[Agda] Using Haskell randomRIO functions from Agda

[Nils Anders Danielsson]

On 2021-10-16 13:13, Serge Leblanc wrote:
>    randomRIO : Char → Char → IO Char
>    randomRIO lo hi = lift (primRandomRIO lo hi) where
> 
>      postulate
>        primRandomRIO : Char → Char → Prim.IO Char

This postulate takes four arguments, lo, hi and the two unnamed
characters. Here is one way to fix your code:

   randomRIO : Char → Char → IO Char
   randomRIO lo hi = lift primRandomRIO
     where

     postulate
       primRandomRIO : Prim.IO Char

     {-# FOREIGN GHC import qualified System.Random as Random #-}
     {-# COMPILE GHC primRandomRIO = \l h -> Random.randomRIO (l , h) #-}

-- 
/NAD