← Back

Modules

CategoricalCrypto

  • CategoricalCrypto
  • Channel.Category
  • Channel.Core
  • Channel.Selection
  • Examples.Basic
  • Examples.Commitment
  • Examples.Signatures
  • Machine.Constraints
  • Machine.Core
  • SFunM

Categories

  • Discrete
  • FreeMonoidal
  • FreeStrictMonoidal
  • GradedKleisli
  • MonoidalCoherence
  • NaturalTransformationHelper
  • Properties

Class

  • Monad.Ext
12345678910111213141516
------------------------------------------------------------------------
-- The Agda standard library
--
-- Characters
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Char where
 
------------------------------------------------------------------------
-- Re-export base definitions and decidability of equality
 
open import Data.Char.Base public
open import Data.Char.Properties
using (_≈?_; _≟_; _<?_; _≤?_; _==_) public