This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

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