Characters

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2023-10-21.

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

Recent changes