/usr/share/agda-stdlib/Data/Char.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Characters
------------------------------------------------------------------------
module Data.Char where
open import Data.Nat using (ℕ)
import Data.Nat.Properties as NatProp
open import Data.Bool using (Bool; true; false)
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.On as On
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe
------------------------------------------------------------------------
-- The type
postulate
Char : Set
{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}
------------------------------------------------------------------------
-- Operations
private
primitive
primCharToNat : Char → ℕ
primCharEquality : Char → Char → Bool
toNat : Char → ℕ
toNat = primCharToNat
infix 4 _==_
_==_ : Char → Char → Bool
_==_ = primCharEquality
_≟_ : Decidable {A = Char} _≡_
s₁ ≟ s₂ with s₁ == s₂
... | true = yes trustMe
... | false = no whatever
where postulate whatever : _
setoid : Setoid _ _
setoid = PropEq.setoid Char
decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_
-- An ordering induced by the toNat function.
strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = On.strictTotalOrder NatProp.strictTotalOrder toNat
|