module Data.ForeignNat.Show where

open import Data.ForeignNat

open import Data.Char  
import Foreign.Haskell as H
open import Data.String
open import Data.Nat
open import Data.Function

{-# IMPORT Data.ForeignNat.Impl #-}

postulate
  showForeign : ℕ′ → H.Colist Char

{-# COMPILED showForeign (Prelude.show . Data.ForeignNat.Impl.unpack) #-}

show : ℕ → Costring
show = H.toColist ∘ showForeign ∘ marshalℕ