[Agda] strict total order on characters

[Nils Anders Danielsson]

On 2011-11-18 12:53, Ramana Kumar wrote:
> 1. (How) Can I show that (_≡_ on Data.Char.toNat) is the same as _≡_?

This depends on what you mean by "the same". You can't prove that they
are propositionally equal.

> 2. Would code achieving the above not be appropriate for the standard
> library? And (probably using it) an ordering on strings too?

Yes. Yes.

> 3. Do you have any comments whatsoever on how to improve the style and
> clarity (given that this was written by a novice)?

I might write something like this:

   module Data.Char where

   …

   import Data.Nat as Nat
   import Data.Nat.Properties as NatProp
   open import Function
   open import Relation.Binary
   import Relation.Binary.On as On

   …

   -- A strict total ordering of characters.

   strictTotalOrder : StrictTotalOrder _ _ _
   strictTotalOrder = record
      { _<_                = Nat._<_ on toNat
      ; isStrictTotalOrder =
          On.isStrictTotalOrder toNat
            (StrictTotalOrder.isStrictTotalOrder
               NatProp.strictTotalOrder)
      }

-- 
/NAD