{-# 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 ( <ᵇ n) ∧ (n <ᵇ ) then
                just (n ∸ )
              else
                nothing

fromNat : Nat → Maybe Char
fromNat n = if ( ≤? n) ∧ (n <ᵇ ) then
              just (C.primNatToChar (n + ))
            else
              nothing

lenLeadingNat : List Char → Nat
lenLeadingNat [] = 
lenLeadingNat (x ∷ xs) = if C.primIsDigit x then
                           suc (lenLeadingNat xs)
                         else