------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for Characters
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Data.Char.Base where

open import Agda.Builtin.String using (primShowChar)
open import Data.Nat.Base    using ()
open import Data.Bool.Base   using (Bool)
open import Data.String.Base using (String)

------------------------------------------------------------------------
-- Re-export the type

import Agda.Builtin.Char as AgdaChar
open AgdaChar using (Char) public

------------------------------------------------------------------------
-- Primitive operations

open AgdaChar

show : Char  String
show = primShowChar

isLower : Char  Bool
isLower = primIsLower

isDigit : Char  Bool
isDigit = primIsDigit

isAlpha : Char  Bool
isAlpha = primIsAlpha

isSpace : Char  Bool
isSpace = primIsSpace

isAscii : Char  Bool
isAscii = primIsAscii

isLatin1 : Char  Bool
isLatin1 = primIsLatin1

isPrint : Char  Bool
isPrint = primIsPrint

isHexDigit : Char  Bool
isHexDigit = primIsHexDigit

toNat : Char  
toNat = primCharToNat

fromNat :   Char
fromNat = primNatToChar