Characters

module primitives.characters where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.universe-levels

Idea

The Char type represents a character. Agda provides primitive functions to manipulate them. Characters are written between single quotes, e.g. 'a'.

Definitions

postulate Char : UU lzero
{-# BUILTIN CHAR Char #-}

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