{-# OPTIONS --without-K --safe #-} module Prelude.Char where open import Agda.Builtin.Char as C public using (Char) open import Agda.Builtin.Nat open import Prelude.Maybe open import Prelude.Bool open import Prelude.Nat open import Prelude.List toUpper toLower : Char → Char toUpper = C.primToUpper toLower = C.primToLower toNat : Char → Maybe Nat toNat c = let n = C.primCharToNat c in if (47 <ᵇ n) ∧ (n <ᵇ 58) then just (n ∸ 48) else nothing fromNat : Nat → Maybe Char fromNat n = if (0 ≤? n) ∧ (n <ᵇ 10) then just (C.primNatToChar (n + 48)) else nothing lenLeadingNat : List Char → Nat lenLeadingNat [] = 0 lenLeadingNat (x ∷ xs) = if C.primIsDigit x then suc (lenLeadingNat xs) else 0