From 1b374761f93fdb97c717a74e747f503851c73dea Mon Sep 17 00:00:00 2001
From: viktorcsimma <csimmaviktor03@gmail.com>
Date: Sat, 2 Mar 2024 11:28:00 +0100
Subject: [PATCH] Adding Haskell.Data.Char.agda

---
 lib/Haskell/Data/Char.agda | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 lib/Haskell/Data/Char.agda

diff --git a/lib/Haskell/Data/Char.agda b/lib/Haskell/Data/Char.agda
new file mode 100644
index 00000000..05b44507
--- /dev/null
+++ b/lib/Haskell/Data/Char.agda
@@ -0,0 +1,29 @@
+module Haskell.Data.Char where
+
+open import Agda.Builtin.Char
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Int using (pos)
+open import Haskell.Prim.Int
+open import Haskell.Prim using (_∘_; eqNat)
+
+-- Translating builtin, postulated Agda functions
+-- to Haskell functions in Data.Char.
+
+isLower isDigit isAlpha isSpace isAscii
+  isLatin1 isPrint isHexDigit : Char → Bool
+isLower = primIsLower
+isDigit = primIsDigit
+isAlpha = primIsAlpha
+isSpace = primIsSpace
+isAscii = primIsAscii
+isLatin1 = primIsLatin1
+isPrint = primIsPrint
+isHexDigit = primIsHexDigit
+toUpper toLower : Char → Char
+toUpper = primToUpper
+toLower = primToLower
+ord : Char → Int
+ord = (integerToInt ∘ pos) ∘ primCharToNat
+chr : Int → Char
+chr = primNatToChar ∘ unsafeIntToNat