Characters

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

Created on 2023-04-27.
Last modified on 2026-05-02.

module primitives.characters where

open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import foundation-core.booleans

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

External links

• Character at Wikidata

Recent changes

• 2026-05-02. Fredrik Bakke and Egbert Rijke. Remove dependency between BUILTIN and postulates (#1373).
• 2025-10-31. Fredrik Bakke. chore: Concepts in primitives (#1653).
• 2023-10-21. Egbert Rijke and Fredrik Bakke. Formatting of postulates (#870).
• 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).