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ℕ