{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Char.Properties where

open import Agda.Builtin.Char
open import Agda.Builtin.Equality

primitive

  primCharToNatInjective :  a b  primCharToNat a  primCharToNat b  a  b