------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for Characters
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Char.Base where
import Data.Nat.Base as ℕ using (_<_; _≡ᵇ_)
open import Data.Bool.Base using (Bool)
open import Function.Base using (_on_)
open import Level using (zero)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_)
open import Relation.Binary.Construct.Closure.Reflexive using (ReflClosure)
------------------------------------------------------------------------
-- Re-export the type, and renamed primitives
open import Agda.Builtin.Char public using ( Char )
renaming
-- testing
( primIsLower to isLower
; primIsDigit to isDigit
; primIsAlpha to isAlpha
; primIsSpace to isSpace
; primIsAscii to isAscii
; primIsLatin1 to isLatin1
; primIsPrint to isPrint
; primIsHexDigit to isHexDigit
-- transforming
; primToUpper to toUpper
; primToLower to toLower
-- converting
; primCharToNat to toℕ
; primNatToChar to fromℕ
)
open import Agda.Builtin.String public using ()
renaming ( primShowChar to show )
infix 4 _≈_ _≉_
_≈_ : Rel Char zero
_≈_ = _≡_ on toℕ
_≉_ : Rel Char zero
_≉_ = _≢_ on toℕ
infix 4 _≈ᵇ_
_≈ᵇ_ : (c d : Char) → Bool
c ≈ᵇ d = toℕ c ℕ.≡ᵇ toℕ d
infix 4 _<_
_<_ : Rel Char zero
_<_ = ℕ._<_ on toℕ
infix 4 _≤_
_≤_ : Rel Char zero
_≤_ = ReflClosure _<_
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4