------------------------------------------------------------------------ -- The Agda standard library -- -- Basic definitions for Characters ------------------------------------------------------------------------ module Data.Char.Core where ------------------------------------------------------------------------ -- The type open import Agda.Builtin.Char public using (Char)