    {-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
                --no-sized-types --no-guardedness --level-universe #-}

    module Agda.Builtin.Char where

    open import Agda.Builtin.Nat
    open import Agda.Builtin.Bool

    postulate Char : Set
    {-# BUILTIN CHAR Char #-}

    primitive
      primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii
        primIsLatin1 primIsPrint primIsHexDigit : Char → Bool
      primToUpper primToLower : Char → Char
      primCharToNat : Char → Nat
      primNatToChar : Nat → Char
      primCharEquality : Char → Char → Bool